mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-10 05:03:59 -05:00
Remove warn_error(+8) from _tags
This commit is contained in:
parent
8076c06047
commit
f20b212b72
1 changed files with 0 additions and 1 deletions
1
_tags
1
_tags
|
|
@ -29,7 +29,6 @@ true: inline(100), optimize(3), unbox_closures, unbox_closures_factor(20)
|
|||
<src/smt/type_smt.*>: package(dolmen)
|
||||
|
||||
# more warnings
|
||||
<src/**/*.ml>: warn_error(+8)
|
||||
<src/**/*.ml>: warn_K, warn_Y, warn_X
|
||||
<src/**/*.ml>: short_paths, safe_string, strict_sequence
|
||||
<src/**/*.cm*>: debug
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue