-
Notifications
You must be signed in to change notification settings - Fork 161
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
set an exit code in
make_doc
(#5835)
For that, - redirect the `Info` output generated by GAPDoc functions to a string, - extract the messages that describe warnings; according to frankluebeck/GAPDoc/commit/826c091491438c1f6ba1f330d17914f45b4bd3af, these are the lines starting with `"#W "`, - omit the LaTeX warnings about overfull boxes (I think we do not want to force ourselves to create manuals without these warning), - report failure if the set of remaining warnings is nonempty.
- Loading branch information
1 parent
ff53a46
commit 37a8938
Showing
1 changed file
with
28 additions
and
5 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters