aboutsummaryrefslogtreecommitdiff
path: root/ci/test.sh
diff options
context:
space:
mode:
authorErik Martin-Dorel2020-04-29 01:19:52 +0200
committerErik Martin-Dorel2020-04-29 01:59:50 +0200
commit94c6da5c8c9db07f406cd28ca9d6532d09b9df15 (patch)
treefb2fec91d14f0321f6f771fa493fc1fe3d49ebfc /ci/test.sh
parentb3fb85c3da48e61bea57aacdd2d0a9468cea9d72 (diff)
fix: coq-tests.el and related files
* The "./test1.v" relative filename triggered an issue => use (coq-test-full-path "test1.v") * The (coq-test-cmd "...") was not optimal for coq-test-print => use (progn (coq-test-goto-before "(*some-unique-identifier*)") (proof-goto-point) (proof-shell-wait)) * The (string-trim "...") function was not defined in batch mode => use (require 'subr-x) & Remove forgotten "(setq temp" snippet.
Diffstat (limited to 'ci/test.sh')
-rwxr-xr-xci/test.sh5
1 files changed, 3 insertions, 2 deletions
diff --git a/ci/test.sh b/ci/test.sh
index 3d9b4a72..50d07579 100755
--- a/ci/test.sh
+++ b/ci/test.sh
@@ -32,7 +32,8 @@ assert emacs --version
rootdir=$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && cd .. && pwd )
srcdir=$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )
-# form="(message \"OK\")"
-form="(progn (add-to-list 'load-path \"$rootdir\") (add-to-list 'load-path \"$srcdir\"))"
+form="(progn (add-to-list 'load-path \"$rootdir\")
+(add-to-list 'load-path \"$srcdir\")
+(setq coq-test-dir \"$srcdir/\"))" # we need a trailing slash here
assert emacs --batch -l ert --eval "$form" -l init-tests.el -l proof-general.el -l coq-tests.el -f ert-run-tests-batch-and-exit