aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-11-04 02:43:04 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-11-04 02:43:04 +0000
commit26c7b886242f2de495f118967724e75f567681c6 (patch)
tree3df6e864f64481efce8e198e9a6e12fff91916ce /Makefile
parentc323245bc688612691a7bd3306f7ca019dcd62aa (diff)
pour que make clean efface ide/utf8_convert.ml venant d'un .mll
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4786 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile1
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index 83d9e79da..a15e0dccb 100644
--- a/Makefile
+++ b/Makefile
@@ -456,6 +456,7 @@ ide/utils/%.cmx: ide/%.ml
clean::
rm -f ide/extract_index.ml ide/find_phrase.ml ide/highlight.ml
rm -f ide/config_lexer.ml ide/config_parser.mli ide/config_parser.ml
+ rm -f ide/utf8_convert.ml
rm -f $(COQIDEBYTE) $(COQIDEOPT)
# coqc