diff options
| author | Emilio Jesus Gallego Arias | 2019-10-31 16:02:09 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-10-31 16:02:09 +0100 |
| commit | a1ea0da415df9137576ea60af5f68ae25dfad1b9 (patch) | |
| tree | fa2cb14ef36028f23ab6e8ed53ce3002854427e2 /doc | |
| parent | 49f0201e5570480116a107765a867e99ef9a8bc6 (diff) | |
| parent | a6e7775b67fe8f82d31d16777559940d6675c94d (diff) | |
Merge PR #10997: Implement the unsupported attribute error using the warning system
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 5 |
2 files changed, 8 insertions, 0 deletions
diff --git a/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst b/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst new file mode 100644 index 0000000000..43a748b365 --- /dev/null +++ b/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst @@ -0,0 +1,3 @@ +- The unsupported attribute error is now an error-by-default warning, + meaning it can be disabled (`#10997 + <https://github.com/coq/coq/pull/10997>`_, by Gaëtan Gilbert). diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index ae9d284661..dd65d4aeb3 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1556,6 +1556,11 @@ the following attributes names are recognized: now foo. Abort. +.. warn:: Unsupported attribute + + This warning is an error by default. It is caused by using a + command with some attribute it does not understand. + .. [1] This is similar to the expression “*entry* :math:`\{` sep *entry* :math:`\}`” in standard BNF, or “*entry* :math:`(` sep *entry* |