aboutsummaryrefslogtreecommitdiff
path: root/dune
diff options
context:
space:
mode:
authorThéo Zimmermann2018-10-11 17:45:58 +0200
committerThéo Zimmermann2018-10-11 17:45:58 +0200
commit132343514c811e9791d8b5f31de5be8906fab66c (patch)
treeaf65a587474338e6d6c378517bee8a14096af3e7 /dune
parent868d5cd983318bff00292329a3920c3b65eb3ada (diff)
parent9e39d88ffb5829a9e2c82fbf54c0765a819b3e5e (diff)
Merge PR #8566: [dune] [test-suite] Support for running the test suite with Dune.
Diffstat (limited to 'dune')
-rw-r--r--dune5
1 files changed, 5 insertions, 0 deletions
diff --git a/dune b/dune
index 240550cf94..4e78a2fe3f 100644
--- a/dune
+++ b/dune
@@ -29,3 +29,8 @@
(targets revision)
(deps (:rev-script dev/tools/make_git_revision.sh))
(action (with-stdout-to revision (run %{rev-script}))))
+
+; Use summary.log as the target
+(alias
+ (name runtest)
+ (deps test-suite/summary.log))