diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-05-27 16:00:53 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-05-28 12:52:55 +0200 |
| commit | 149b0c422027a31972b62457af1bf97bd016e26c (patch) | |
| tree | 32f5267f4f24086018d1c04e71a236392f089993 /test-suite/coq-makefile | |
| parent | 2eb27e56ea4764fa2f2acec6f951eef2642ff1be (diff) | |
Gitlab CI
Diffstat (limited to 'test-suite/coq-makefile')
| -rw-r--r-- | test-suite/coq-makefile/template/init.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh index bfd2c1b95..c952d41a3 100644 --- a/test-suite/coq-makefile/template/init.sh +++ b/test-suite/coq-makefile/template/init.sh @@ -1,5 +1,5 @@ -export PATH=../../../bin/:$PATH +export PATH=$COQBIN:$PATH rm -rf theories src Makefile Makefile.conf tmp git clean -dfx || true |