diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-11-15 09:05:13 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-11-15 09:05:13 +0100 |
| commit | 0134ebc3eb6d8f4d6a45adf54f8c6dbf7c4edbca (patch) | |
| tree | 5d7343d4c0903bf6da1cc24f9b7d016bdbf4736a /test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh | |
| parent | a5d68eacf819959dc277e2e9ef9cc4a3e712f5fe (diff) | |
| parent | 360d28670511d51c2b63692c9ce0f7ebe5f1ae3e (diff) | |
Merge PR #6122: Remove dependency of test-suite on git (fix #5725).
Diffstat (limited to 'test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh')
| -rwxr-xr-x | test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh | 2 |
1 files changed, 0 insertions, 2 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/ |