diff --git a/_tags b/_tags index 831c1ef..825dc26 100644 --- a/_tags +++ b/_tags @@ -32,4 +32,4 @@ true: bin_annot, color(always) : warn(-33) true: mark_tag_used <**/*.cmx>: optimize(3) -: nolabels +: nolabels diff --git a/src/SequenceLabels.ml b/src/SequenceLabels.ml new file mode 100644 index 0000000..fb15e92 --- /dev/null +++ b/src/SequenceLabels.ml @@ -0,0 +1 @@ +include Sequence diff --git a/src/sequenceLabels.ml b/src/sequenceLabels.ml deleted file mode 120000 index b990b32..0000000 --- a/src/sequenceLabels.ml +++ /dev/null @@ -1 +0,0 @@ -Sequence.ml \ No newline at end of file