aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-11-26 09:37:15 -0500
committerGravatar Jason Gross <jgross@mit.edu>2017-11-26 09:37:15 -0500
commit76582484c3a9c822619f9f52fdc8d5677958ef90 (patch)
tree111b3603b39da42f4cb693c77ff704442838c3ac /Makefile
parent5dbccd33123542384b4cfb5436324181c5b13148 (diff)
Add src/Specific/.autgenerated-deps to clean target
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index a653be996..c867519f9 100644
--- a/Makefile
+++ b/Makefile
@@ -376,7 +376,7 @@ test: $(RUN_TEST_BINARIES)
selected-test: $(RUN_SELECTED_TEST_BINARIES)
clean::
- rm -f Makefile.coq remake_curves.log
+ rm -f Makefile.coq remake_curves.log src/Specific/.autgenerated-deps
cleanall:: clean clean-coqprime