mirror of
https://github.com/c-cube/iter.git
synced 2025-12-07 03:35:32 -05:00
detail in _tags
This commit is contained in:
parent
9a198455df
commit
74fc940f3e
1 changed files with 1 additions and 0 deletions
1
_tags
1
_tags
|
|
@ -29,3 +29,4 @@
|
||||||
# OASIS_STOP
|
# OASIS_STOP
|
||||||
true: bin_annot
|
true: bin_annot
|
||||||
<**/*.ml>: warn_A, warn(-4)
|
<**/*.ml>: warn_A, warn(-4)
|
||||||
|
true: mark_tag_used
|
||||||
|
|
|
||||||
Loading…
Add table
Reference in a new issue