diff options
| author | Gaëtan Gilbert | 2019-07-21 17:05:07 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-07-21 17:05:48 +0200 |
| commit | f1206ec5d6c6d7f557ec6802e64b41d82fc806f8 (patch) | |
| tree | cd0316b3bbbb7f85a5d77b3fdf38ee0d413047cc /dev | |
| parent | cd6fc50854285f02bf151e94bdfb819988531fd2 (diff) | |
Dune: fix build_all_stdlib rule
The issue could be reproduced by doing "dune build
test-suite/misc/universes/all_stdlib.v" (from a clean build) which
would error 127 with no message.
- only redirect stdout so that in the future we will see error
messages
- put the script as a dependency (I guess it sometime succeeded when
copying the deps for the test suite happened before running it)
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions