aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar monate <monate@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-05-14 16:21:44 +0000
committerGravatar monate <monate@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-05-14 16:21:44 +0000
commita020f056c15a274385183d22af2132f430868b2b (patch)
tree9dff9909b2f7570ddedf5453b2fc2f30f062076e /Makefile
parent05c1e8d802c326b28db14483390af2d83bd6d19a (diff)
coqide: .* on start/add \n on eof
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4022 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 36545e5bd..cc7bfe1dc 100644
--- a/Makefile
+++ b/Makefile
@@ -400,7 +400,7 @@ beforedepend:: ide/config_parser.mli ide/config_parser.ml
beforedepend:: ide/utf8_convert.ml
FULLIDELIB=$(FULLCOQLIB)/ide
-IDEFILES=ide/coq.png ide/.coqide-gtk2rc
+IDEFILES=ide/coq.png ide/.coqide-gtk2rc ide/FAQ
ide: $(COQIDEBYTE) $(COQIDE) states
clean-ide: