| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Contributors are *not* required to prepare all the patches by
themselves. They can request help from project authors, who should be
ready to take part in this.
Also, finish replacing "development" by the more appropriate word
"project".
|
|
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
|
|
Thanks to @Zimmi48 as always for the careful review.
Co-Authored-By: ejgallego <e+git@x80.org>
|
|
|
|
|
