From 4dfefc95424528e89f6158671ff398bd85b1efa4 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Tue, 26 Dec 2017 17:11:31 +0100
Subject: [PATCH] Move check_realization.sh from nightly to bench.

---
 Makefile.in                           | 1 +
 bench/bench                           | 3 +++
 {misc => bench}/check_realizations.sh | 0
 misc/nightly-bench.sh                 | 3 ---
 4 files changed, 4 insertions(+), 3 deletions(-)
 rename {misc => bench}/check_realizations.sh (100%)

diff --git a/Makefile.in b/Makefile.in
index ba5f16b43..47b374010 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -1589,6 +1589,7 @@ bench:: bin/why3.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS) \
 	# if test -d examples/runstrat ; then \
 	#  $(MAKE) test-runstrat.@OCAMLBEST@ ; fi
 	bash bench/bench ".@OCAMLBEST@"
+	@echo ""
 	@if test "@enable_coq_tactic@" = "yes"; then \
 	   echo "=== checking the Coq tactic ==="; \
 	   $(MAKE) test-coq-tactic; fi
diff --git a/bench/bench b/bench/bench
index 57ba1ab53..e1ef446b1 100755
--- a/bench/bench
+++ b/bench/bench
@@ -254,3 +254,6 @@ list_stuff --list-formats
 list_stuff --list-metas
 list_stuff --list-debug-flags
 echo ""
+
+echo "=== Checking realizations ==="
+exec bench/check_realizations.sh
diff --git a/misc/check_realizations.sh b/bench/check_realizations.sh
similarity index 100%
rename from misc/check_realizations.sh
rename to bench/check_realizations.sh
diff --git a/misc/nightly-bench.sh b/misc/nightly-bench.sh
index e988d48b8..3abca78e5 100755
--- a/misc/nightly-bench.sh
+++ b/misc/nightly-bench.sh
@@ -137,9 +137,6 @@ else
     echo "Counterexample regression tests succeeded. " >> $REPORT
 fi
 
-# check realizations
-misc/check-realizations.sh >> $REPORT
-
 # replay proofs
 examples/regtests.sh &> $OUT
 if test "$?" != "0" ; then
-- 
GitLab