On 3 August 2015 at 10:30, Thomas Gazagnaire <[email protected]> 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 _______________________________________________ opam-devel mailing list [email protected] http://lists.ocaml.org/listinfo/opam-devel
