Merge branch 'jk/clone-local'

Merge branch 'jk/clone-local'

"git clone --local $path" started its life as an experiment to
optionally use link/copy when cloning a repository on the disk, but
we didn't deprecate it after we made the option a no-op to always
use the optimization.

The command learns "--no-local" option to turn this off, as a more
explicit alternative over use of file:// URL.

* jk/clone-local:
  clone: allow --no-local to turn off local optimizations
  docs/clone: mention that --local may be ignored