Closed fingolfin closed 2 years ago
Merging #29 (041a498) into master (2d678ae) will not change coverage. The diff coverage is
n/a
.
@@ Coverage Diff @@
## master #29 +/- ##
=======================================
Coverage 94.32% 94.32%
=======================================
Files 24 24
Lines 7573 7573
=======================================
Hits 7143 7143
Misses 430 430
Add 'set -e' so that errors abort the script (otherwise it is very easy to miss if some step of the process fails).
Also switch to using pdftex to produce a .pdf version of the manual.