aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.common
diff options
context:
space:
mode:
authorGravatar lmamane <lmamane@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-02-22 13:39:13 +0000
committerGravatar lmamane <lmamane@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-02-22 13:39:13 +0000
commite8ef565dadd110329f806fa3c281055fcd807440 (patch)
treee0f069cb228ee77524800d98c53291014c1a1315 /Makefile.common
parent2e67ff1b33d05b9efc020de664f3200f9ff0d479 (diff)
Merge with lmamane's private branch:
- New vernac command "Delete" - New vernac command "Undo To" - Added a few hooks used by new contrib/interface - Beta/incomplete version of dependency generation and dumping git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10580 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common3
1 files changed, 2 insertions, 1 deletions
diff --git a/Makefile.common b/Makefile.common
index f63d7dbcb..1b7a2fef5 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -353,7 +353,8 @@ INTERFACE:=\
contrib/interface/history.cmo \
contrib/interface/name_to_ast.cmo contrib/interface/debug_tac.cmo \
contrib/interface/showproof_ct.cmo contrib/interface/showproof.cmo \
- contrib/interface/blast.cmo contrib/interface/centaur.cmo
+ contrib/interface/blast.cmo contrib/interface/depends.cmo \
+ contrib/interface/centaur.cmo
INTERFACECMX:=$(INTERFACE:.cmo=.cmx)