Commits on Apr 20, 2021

1. 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.

   

   fingolfin committed Apr 20, 2021
   Configuration menu

   • View commit details
   • Copy full SHA for 56715c3
   • Browse repository at this point

   Copy the full SHA

   56715c3 View commit details

   Browse the repository at this point in the history