diff options
author | 2000-11-09 13:20:56 +0000 | |
---|---|---|
committer | 2000-11-09 13:20:56 +0000 | |
commit | 6422b5dd14a61417e97ec9b4b06df726a70cfc21 (patch) | |
tree | c0edea0f8b59dc97987b9e54644e4eb54af10fac /tools | |
parent | fb5191cdcf7847df0967ddf5bc0e91b256d44bac (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.ml | 8 |
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" |