diff options
| -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 288d8a035c..2c9185349d 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" |