Improve the infrastructure scripts #815

Chris00 opened this Issue Aug 3, 2016 · 1 comment


None yet

1 participant

Chris00 commented Aug 3, 2016 edited
  • The infrastructure scripts should be under version control.
  • The scripts should be improved to open an issue when something goes wrong. (Github will then forward mails.)
  • A daily rebuild from scratch with various compilers should take place (with Github error reporting). The idea is to perform that the site is easily buildable by users with the recommended versions of the compiler.
  • Automatically report (opening a Github issue) when there is a problem with the package list.
@pw374 pw374 changed the title from Inprove the infrastructure scripts to Improve the infrastructure scripts Sep 21, 2016
Chris00 commented Nov 21, 2016
@Chris00 Chris00 self-assigned this Dec 6, 2016
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment