Re: git is live

Tom Tromey
2013-10-23T13:13:30Z

DJ> Note that this has broken my robo-merge scripts for libiberty. I hope
DJ> that cvs's libiberty/ and include/ can be re-enabled, assuming there are
DJ> other users of libiberty left in src.

I fixed this. I believe only 'include' was disabled. 'libiberty' isn't
(and apparently never was) mentioned in the commitinfo file.

Tom