[opam-devel] On the new mixed mode pins

[Thomas Leonard]

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)?
>>
>> 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?

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