From 728216337e2541b37135d86c1b0206706cf4ed1a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 19 Feb 2019 18:23:42 +0100
Subject: [coq_makefile] Enforce warn_error for plugins.

The amount of dangerous warnings in plugins is out of hand, including
some very serious ones.

As Coq developers are maintaining plugins these days it makes sense to
require the contributions to follow the same coding discipline as in
the main tree, thus we require the set of warnings fatal warnings to
be the same in Coq and in plugins.

We don't mark deprecation as fatal as to allow time for migration.

Fixes #6974
---
 doc/sphinx/practical-tools/utilities.rst | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'doc')

diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index 8346b72cb9..35231610fe 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -144,6 +144,10 @@ Here we describe only few of them.
 :CAMLFLAGS:
    can be used to specify additional flags to the |OCaml|
    compiler, like ``-bin-annot`` or ``-w``....
+:OCAMLWARN:
+   it contains a default of ``-warn-error +a-3``, useful to modify
+   this setting; beware this is not recommended for projects in
+   Coq's CI.
 :COQC, COQDEP, COQDOC:
    can be set in order to use alternative binaries
    (e.g. wrappers)
-- 
cgit v1.2.3