Commit 388c171f authored by Christian Engwer's avatar Christian Engwer

[!706] Document the --skipversioncheck option of dunecontrol

Merge branch 'document-skipversioncheck' into 'master'

ref:core/dune-common Apparently, this option has been around since 2009, but
somehow it never made it into the man page and the output of -h.

See merge request [!706]

  [!706]: gitlab.dune-project.org/core/dune-common/merge_requests/706
parents 48d79b69 95f954d7
Pipeline #21137 passed with stage
in 5 minutes and 49 seconds
......@@ -742,6 +742,7 @@ usage () {
echo " --resume resume a previous run (only consider the modules"
echo " not built successfully on the previous run)"
echo " --skipfirst skip the first module (use with --resume)"
echo " --skipversioncheck do not perform version checks when looking for other Dune modules"
echo " --opts=FILE load default options from FILE"
echo " --builddir=NAME make out-of-source builds in a subdir NAME."
echo " This directory is created inside each module."
......
......@@ -136,6 +136,10 @@ Resume a previous run (only consider the modules not built successfully on the p
.IP
Skip the first module (use with --resume)
.HP
\fB--skipversioncheck\fP
.IP
When looking for Dune modules, do not check whether they have the required versions
.HP
\fB--opts=\fP\fIfile\fP
.IP
Load default options from \fIfile\fP
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment