aboutsummaryrefslogtreecommitdiffhomepage
path: root/.merlin
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2016-06-25 15:58:19 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2016-06-25 16:07:28 +0200
commit799b4028834c1b073db8349bf75e384750fed591 (patch)
treeec911e8f178badfb1360d44ff8004fc4ba74d7a2 /.merlin
parent4d4e2f421c1a4f0339568d3c96ff2459a027aa09 (diff)
[merlin] Fix .merlin STM includes.
Diffstat (limited to '.merlin')
-rw-r--r--.merlin6
1 files changed, 5 insertions, 1 deletions
diff --git a/.merlin b/.merlin
index 91dbc336b..7ae642233 100644
--- a/.merlin
+++ b/.merlin
@@ -1,4 +1,4 @@
-FLG -rectypes
+FLG -rectypes -thread
S config
B config
@@ -26,6 +26,8 @@ S printing
B printing
S parsing
B parsing
+S stm
+B stm
S toplevel
B toplevel
@@ -35,3 +37,5 @@ S tools/coqdoc
B tools/coqdoc
S dev
B dev
+
+PKG threads.posix