diff options
| author | Théo Zimmermann | 2017-11-08 15:29:56 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2017-11-08 15:30:05 +0100 |
| commit | 360d28670511d51c2b63692c9ce0f7ebe5f1ae3e (patch) | |
| tree | 7959b2b28472bdb345d9b2826c1b6686c08c5744 /dev/base_include | |
| 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 'dev/base_include')
0 files changed, 0 insertions, 0 deletions