diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-07-04 15:49:04 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-07-05 11:28:33 +0200 |
| commit | 353669f8f175adabf878be0334a1979c439778af (patch) | |
| tree | 2330810fd90ee6577f73c13d7dc5d0f69a2e96de | |
| parent | df076edfe673069decf9e8b0dc5f3b7941796060 (diff) | |
| download | compcert-353669f8f175adabf878be0334a1979c439778af.tar.gz compcert-353669f8f175adabf878be0334a1979c439778af.zip | |
Re-enable `deprecated-hint-rewrite-without-locality` warning
No longer triggered since commit df076edfe.
| -rw-r--r-- | Makefile | 3 |
1 files changed, 1 insertions, 2 deletions
@@ -64,8 +64,7 @@ endif COQCOPTS ?= \ -w -undeclared-scope \ -w -unused-pattern-matching-variable \ - -w -deprecated-ident-entry \ - -w -deprecated-hint-rewrite-without-locality + -w -deprecated-ident-entry cparser/Parser.vo: COQCOPTS += -w -deprecated-instance-without-locality |