[opam-devel] On the new mixed mode pins
thomas at gazagnaire.org
Mon Aug 3 10:30:07 BST 2015
>> FWIW this just happened to me, lost an hour and half banging my head on the table (that may have helped with other things though).
> How about moving mixed mode to "path" instead of "git" (as I think
> someone suggested before)?
> "git pin -k path ..." (or just "git pin") will use mixed mode if possible
> "git pin -k git ..." uses the Git commit, ignoring the working tree
To avoid ambiguity: `git pin -k mixed` maybe?
More information about the opam-devel