aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coq_makefile.ml
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-07-16 14:15:03 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-07-16 14:15:03 +0000
commit0fb97de232866adbec1d7eb14e33fa4a7b15fc31 (patch)
tree7f2d3e95f3f11be5dc60a810dbaa0ce5e52ffa19 /tools/coq_makefile.ml
parent4b920ae3c82f857944ea09a22ec74e972a498332 (diff)
all.g.ps -> all-gal.ps
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1855 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coq_makefile.ml')
-rw-r--r--tools/coq_makefile.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index dd4a51365..9f1e178a5 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -279,7 +279,7 @@ let all_target l =
print "gallinahtml: $(GHTMLFILES)\n\n";
print "all.ps: $(VFILES)\n";
print "\t$(COQWEB) -ps -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n";
- print "all.g.ps: $(GFILES)\n";
+ print "all-gal.ps: $(GFILES)\n";
print "\t$(COQWEB) -ps -o $@ `$(COQDEP) -sort -suffix .g $(VFILES)`\n\n";
print "xml:: .xml_time_stamp\n";
print ".xml_time_stamp: "; print_list "\\\n " (vofiles l);