diff options
| author | Théo Zimmermann | 2018-12-23 17:37:28 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2018-12-26 23:48:02 +0100 |
| commit | 3d833269860ae9fe8e6f4a3d936d23404afe453e (patch) | |
| tree | 7b8eaac774d8f5828c97f5f958140e679865f539 /dev/ci/ci-plugin_tutorial.sh | |
| parent | b878216ca5e85f8164fa098b9dc0e688a212072d (diff) | |
[dune] Build refman with fatal warnings by default like in the Makefile build.
The way to override this default is not exactly the same as in the legacy Makefile
but it has been documented as well.
Diffstat (limited to 'dev/ci/ci-plugin_tutorial.sh')
0 files changed, 0 insertions, 0 deletions