diff options
Diffstat (limited to 'Makefile.make')
| -rw-r--r-- | Makefile.make | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/Makefile.make b/Makefile.make index 34f5707ae8..2f6781439c 100644 --- a/Makefile.make +++ b/Makefile.make @@ -253,7 +253,6 @@ docclean: archclean: clean-ide optclean voclean plugin-tutorialclean rm -rf _build _build_boot - rm -f $(ALLSTDLIB).* optclean: rm -f $(COQTOPEXE) $(CHICKEN) $(TOPBINOPT) |