[opam-devel] On the new mixed mode pins

Thomas Gazagnaire 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)?
> 
> i.e.
> 
> "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 mailing list