diff options
Diffstat (limited to 'Makefile')
-rw-r--r-- | Makefile | 1 |
1 files changed, 0 insertions, 1 deletions
@@ -223,7 +223,6 @@ cleanconfig: distclean: clean cleanconfig voclean: - rm -f states/*.coq find theories plugins test-suite -name '*.vo' -o -name '*.glob' | xargs rm -f devdocclean: |