Shortcut for [John Ousterhout].