"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