aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-11-09 13:20:56 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-11-09 13:20:56 +0000
commit6422b5dd14a61417e97ec9b4b06df726a70cfc21 (patch)
treec0edea0f8b59dc97987b9e54644e4eb54af10fac /tools
parentfb5191cdcf7847df0967ddf5bc0e91b256d44bac (diff)
do_Makefile -> coq_makefile pour le bootstrap!
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@835 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
-rw-r--r--tools/coq_makefile.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 288d8a035..2c9185349 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -46,7 +46,7 @@ let section s =
let usage () =
output_string stderr "Usage summary:
-do_Makefile [subdirectory] .... [file.v] ... [file.ml] ... [-custom
+coq_makefile [subdirectory] .... [file.v] ... [file.ml] ... [-custom
command dependencies file] ... [-I dir] ... [VARIABLE = value] ...
[-full] [-no-opt] [-f file] [-o file] [-h] [--help]
@@ -93,7 +93,7 @@ let standard sds =
print "\n";
print "Makefile::\n";
print "\tmv -f Makefile Makefile.bak\n";
- print "\tdo_Makefile -f Make -o Makefile\n";
+ print "\tcoq_makefile -f Make -o Makefile\n";
print "\n";
print "clean::\n";
print "\trm -f *.cmo *.cmi *.cmx *.o *.vo *.vi *~\n";
@@ -348,13 +348,13 @@ let banner () =
let warning () =
print "# WARNING\n#\n";
- print "# This Makefile has been automagically generated by do_Makefile\n";
+ print "# This Makefile has been automagically generated by coq_makefile\n";
print "# Edit at your own risks !\n";
print "#\n# END OF WARNING\n\n"
let command_line args =
print "#\n# This Makefile was generated by the command line :\n";
- print "# do_Makefile ";
+ print "# coq_makefile ";
List.iter (fun x -> print x; print " ") args;
print "\n#\n\n"