Le 2011-05-14 à 21:09, Brad Roberts a écrit :
> I went to each auto-tester and did:
>
> git reset --hard origin/master
> git pull origin
>
> That seems to have brought them all up to the current commit. We'll see if
> the problem crops up again.
If you don't want to see it ever again, replace the pull in the autotester with:
git fetch origin
git reset --hard origin/master
This way you'll have no merge and therefore no conflict.
> Looking at the phobos network on github, I see that HEAD is specifically
> tagged to a specific, non-most-recent, commit,
> and is listed as a branch. Neither druntime nor dmd have those properties.
HEAD is not a branch (normally). Has someone created and pushed a branch called
HEAD to mess with our brains?
I don't think it causes any problem (the real HEAD and the HEAD branch are
distinct), but it's rather misleading. Someone with commit access to the shared
repository should do "git push origin :HEAD" to remove that branch.
--
Michel Fortin
[email protected]
http://michelf.com/
_______________________________________________
phobos mailing list
[email protected]
http://lists.puremagic.com/mailman/listinfo/phobos
