aboutsummaryrefslogtreecommitdiff
path: root/etc/ci/smithers.sh
diff options
context:
space:
mode:
Diffstat (limited to 'etc/ci/smithers.sh')
-rwxr-xr-xetc/ci/smithers.sh2
1 files changed, 2 insertions, 0 deletions
diff --git a/etc/ci/smithers.sh b/etc/ci/smithers.sh
index 2eb804bdd..247ab0690 100755
--- a/etc/ci/smithers.sh
+++ b/etc/ci/smithers.sh
@@ -5,6 +5,8 @@ set -ex
cd "$WORKSPACE"
export PATH="/opt/coq-$coq_version/bin${PATH:+:}$PATH"
. /opt/bashrc/bashrc
+coqtop -v
+echo | coqtop
export TARGETS="coq display bench test"
export TARGETS="coq nonautogenerated-specific nonautogenerated-specific-display" # bench test" # bench and test don't work on smithers
rm -f BUILD.ok