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 /default.nix | |
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 'default.nix')
0 files changed, 0 insertions, 0 deletions