aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorcoq2005-05-25 13:44:00 +0000
committercoq2005-05-25 13:44:00 +0000
commitaa7a5617b266abc8549dc07273238269f8bab1c0 (patch)
treeb50a216ba5c6eef74836f59579d1bf7f677cd63c
parent8464cd8a8df852799da9cb7a1fd94b8faf3cf9c6 (diff)
Forgot to remove a cmo.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7074 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--Makefile1
1 files changed, 0 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index da9c4f1354..49ddef7bdf 100644
--- a/Makefile
+++ b/Makefile
@@ -298,7 +298,6 @@ SUBTACCMO=\
contrib/subtac/scoq.cmo \
contrib/subtac/sast.cmo \
contrib/subtac/infer.cmo \
- contrib/subtac/top_printer.cmo \
contrib/subtac/rewrite.cmo \
contrib/subtac/sparser.cmo