Closed fingolfin closed 8 months ago
Use this to avoid duplicating the package version and release date in doc/guava.xml, removing one potential source for mistakes when doing releases.
The main advantage is that it removes the hard coded path to a GAP executable, and also works correctly with ReleaseTools.
@osj1961 it would be great if you could either
Max, I've merged all three. If you really don't mind doing the release, I'd be grateful. -Joe
Done.
Use this to avoid duplicating the package version and release date in doc/guava.xml, removing one potential source for mistakes when doing releases.
The main advantage is that it removes the hard coded path to a GAP executable, and also works correctly with ReleaseTools.