diff options
| -rw-r--r-- | src/.merlin | 2 | ||||
| -rw-r--r-- | src/_tags | 3 |
2 files changed, 5 insertions, 0 deletions
diff --git a/src/.merlin b/src/.merlin new file mode 100644 index 00000000..a55fccb1 --- /dev/null +++ b/src/.merlin @@ -0,0 +1,2 @@ +S . +B _build/ diff --git a/src/_tags b/src/_tags new file mode 100644 index 00000000..05e3b193 --- /dev/null +++ b/src/_tags @@ -0,0 +1,3 @@ +true: -traverse, debug +<**/*.ml>: bin_annot, annot + |