diff options
Diffstat (limited to 'tuto3/src/dune')
| -rw-r--r-- | tuto3/src/dune | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tuto3/src/dune b/tuto3/src/dune index 6b09d5d98b..ba6d8b288f 100644 --- a/tuto3/src/dune +++ b/tuto3/src/dune @@ -1,6 +1,7 @@ (library (name tuto3_plugin) (public_name coq.plugins.tutorial.p3) + (flags :standard -warn-error -3) (libraries coq.plugins.ltac)) (rule |