diff options
| -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")))) |