diff options
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build index 034c9ea03c..147668187f 100644 --- a/Makefile.build +++ b/Makefile.build @@ -150,7 +150,7 @@ endif ########################################################################### -# This include below will lauch the build of all .d. +# This include below will launch the build of all .d. # The - at front is for disabling warnings about currently missing ones. # For creating the missing .d, make will recursively build things like # coqdep_boot (for the .v.d files) or coqpp (for .mlg -> .ml -> .ml.d). |