diff options
Diffstat (limited to 'doc/general.texi')
| -rw-r--r-- | doc/general.texi | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/doc/general.texi b/doc/general.texi index 9a823d4d8c..3b4b372155 100644 --- a/doc/general.texi +++ b/doc/general.texi @@ -951,9 +951,6 @@ should also be avoided if they don't make the code easier to understand. @item If you add a new file, give it a proper license header. Do not copy and paste it from a random place, use an existing file as template. -@item - If you add a new header or change an existing one, make sure it passes - @code{make checkheaders}. @end enumerate We think our rules are not too hard. If you have comments, contact us. |