diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 568c909edb..7491c1f9af 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -330,6 +330,7 @@ let clean sds sps = if !some_vfile then begin print "\trm -f $(OBJFILES) $(OBJFILES:.o=.native) $(NATIVEFILES)\n"; + print "\tfind . -name .coq-native -type d -empty -delete\n"; print "\trm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)\n" end; print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex\n"; |