On Wed, May 6, 2015 at 4:51 AM, Thomas Braibant <[email protected]>
wrote:
depends: [
> "asn1-combinators" { = "0.1.1" }
> ...
> "foo" { git: "path-to-git/foo#bar"}
> ]
>
This could be very useful. It would also help to allow {path:
$HOME/mycode}. With only git pins, developing multiple repos is still
difficult. You have to push the changes in one repo before testing them
with another repo. Sharing path pins would let multiple developers all work
on multiple repos, but each developer can still have fine control over
exactly what state each of the individual repos is at. The only slight
inconvenience is everyone has to standardize on the paths of their local
working directories, but that's not too bad as along as a $HOME variable
was allowed.
_______________________________________________
Platform mailing list
[email protected]
http://lists.ocaml.org/listinfo/platform
