[opam-devel] On the new mixed mode pins
talex5 at gmail.com
Mon Aug 3 10:45:03 BST 2015
On 3 August 2015 at 10:30, Thomas Gazagnaire <thomas at gazagnaire.org> wrote:
>>> 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?
I think it should either be the default, or "-k path" should be
required for a non-mixed path pin. Plain path pins are almost never
what you want, due to stale oasis files getting reused (hit this
myself just this morning, where I'd forgotten the "-k git" again).
Dr Thomas Leonard http://roscidus.com/blog/
GPG: DA98 25AE CAD0 8975 7CDA BD8E 0713 3F96 CA74 D8BA
More information about the opam-devel