aboutsummaryrefslogtreecommitdiff
path: root/etc
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-11-04 17:34:42 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-11-04 18:21:51 -0400
commit34fe7947da904853bafd5328d0377c7fc23ed2ac (patch)
treee8042eebb3a7c5e67d69fb8eb274690748db16ab /etc
parent9bfbb6ea54390d70a187cd6a1bad4e75c8c437a9 (diff)
Print coq version on smithers
Diffstat (limited to 'etc')
-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