From f1206ec5d6c6d7f557ec6802e64b41d82fc806f8 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sun, 21 Jul 2019 17:05:07 +0200
Subject: 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)
---
 test-suite/misc/universes/dune | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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"))))
-- 
cgit v1.2.3