Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
CI: detect failure to run
make docomp
nicely again
We have a test for our CI which detects if a PR should have run `make docomp`. But we did not reach it anymore since some changes to `bin/BuildPackages.sh` which added code to use GAP to extract the name of any given packages, by letting GAP print it to stdout and grabbing it from there. But in this particular failure scenario, GAP also printed a warning, which caused `BuildPackages.sh` to fail. This patch suppresses that warning.
- Loading branch information