Integrate etc/extract_manuals.py
(and related steps) into the automated GAP release process
#250
Labels
etc/extract_manuals.py
(and related steps) into the automated GAP release process
#250
This has been mentioned in various places already, such as gap-system/gap#4596 (comment), but I think it'll be good to record it here in its own issue.
It might not be completely straightforward to automate putting the extracted manuals onto the web server, and this of course could change, given the resolution to #223.
The text was updated successfully, but these errors were encountered: