diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-08-15 12:00:18 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-08-15 14:22:26 -0400 |
| commit | 23d1504de4111223dc4805c6f4176a4d9e028b79 (patch) | |
| tree | 6607a3128412026d072627e1492f10542fd76856 /tactics/dn.mli | |
| parent | 83e506e9a4b8140320e8f505b9ef6e4da05d710c (diff) | |
Better error messages on the CI
This makes it so that when a ci target fails, we don't get red herring
error messages about .ok files not existing.
Since this requires bash, we make a helper script that invokes bash, so
as to not depend on bash in general.
Diffstat (limited to 'tactics/dn.mli')
0 files changed, 0 insertions, 0 deletions