Gerwin wrote:
> There is another option for the AFP: we could host on github and use the
> mercurial git plugin [https://hg-git.github.io] to work with it as if it was
> a mercurial repo. I don’t have much experience with how stable that option
> is, but it would be free and it would be easy on account management.
I've been using hg-git since 2015, notably for my main private repository. A
quick check on my disk reveals that's how I'm accessing 32 git repositories.
I find that the plugin works well for branch-free repositories. I don't know
what it would do with git branches, and for such repositories I use git
directly.
The main things I noticed about hg-git:
1. The first time you use it it refuses to push. One has to enter
hg bookmark -f master
2. When merging, "hg merge" is never enough; you need e.g. "hg merge tip".
3. Once in a while, I get low level Python errors. That gets sorted out by
updating hg-git. hg-git seems to depend on quite a bit of Python libraries, so
it's easy for them to get out of sync if I update my system.
4. You can't refer to revision numbers directly in your change logs, because
these are different in git and hg.
Jasmin
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
