aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorcharguer2018-11-12 16:28:14 +0100
committerVincent Laporte2019-03-18 10:29:51 +0000
commit7b0b7e8440829f80d1fdee1a7f6daa82d3538c90 (patch)
treeb2596fb20ed95979cee2e92ebfcf3e6ef3e7197a /Makefile
parent9883bde37482632e135895d75fae973ef8b89a08 (diff)
binding generator for coqide
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile1
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index 6adefa5d47..2b5d2cea16 100644
--- a/Makefile
+++ b/Makefile
@@ -263,6 +263,7 @@ clean-ide:
rm -f ide/input_method_lexer.ml
rm -f ide/highlight.ml ide/config_lexer.ml ide/config_parser.mli ide/config_parser.ml
rm -f ide/utf8_convert.ml
+ rm -f ide/default.bindings
rm -rf $(COQIDEAPP)
mlgclean: