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 | |
| 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)
| -rw-r--r-- | test-suite/misc/universes/dune | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/test-suite/misc/universes/dune b/test-suite/misc/universes/dune index 0772f95604..c0d925deb5 100644 --- a/test-suite/misc/universes/dune +++ b/test-suite/misc/universes/dune @@ -1,8 +1,9 @@ (rule (targets all_stdlib.v) (deps + build_all_stdlib.sh (source_tree ../../../theories) (source_tree ../../../plugins)) (action - (with-outputs-to all_stdlib.v + (with-stdout-to all_stdlib.v (bash "./build_all_stdlib.sh")))) |