Gilles Peskine 67ffdafde6 all.sh --outcome-file creates an outcome file
By default, remove the outcome file before starting. With
--append-outcome, append to the existing outcome file if there is one.
2019-09-24 19:21:19 +02:00
..
2019-06-27 08:46:45 +02:00