diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-11-08 15:29:56 +0100 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-11-08 15:30:05 +0100 |
| commit | 360d28670511d51c2b63692c9ce0f7ebe5f1ae3e (patch) | |
| tree | 7959b2b28472bdb345d9b2826c1b6686c08c5744 /test-suite/coq-makefile | |
| parent | d9f79d97dbc503e149cba2df1b228a94d7ac970b (diff) | |
Remove dependency of test-suite on git (fix #5725).
The two lines that this commit remove are spurious as a `git clean -dfx || true`
is already performed in `test-suite/coq-makefile/template/init.sh`.
While this resolves the accidental dependency on git, I am still unhappy with
this call of `git clean -dfx`.
Diffstat (limited to 'test-suite/coq-makefile')
| -rwxr-xr-x | test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh | 2 | ||||
| -rwxr-xr-x | test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh | 2 |
2 files changed, 0 insertions, 4 deletions
diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh index 88606cd47..378573957 100755 --- a/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh +++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh @@ -2,8 +2,6 @@ set -e -git clean -dfx - cat > _CoqProject <<EOT -I src/ diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh index 939ef9c7b..1b57a356b 100755 --- a/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh +++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh @@ -2,8 +2,6 @@ set -e -git clean -dfx - cat > _CoqProject <<EOT -bypass-API -I src/ |