summaryrefslogtreecommitdiff
path: root/.merlin
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-27 16:53:30 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-27 18:33:25 +0100
commit1b92c226e563643da187b8614d5888dc4855eb43 (patch)
treec4c3d204b36468b58cb71050ba95f06b8dd7bc2e /.merlin
parent7c9b0a702976078b813e6493c1284af62a3f093c (diff)
Imported Upstream version 8.6
Diffstat (limited to '.merlin')
-rw-r--r--.merlin10
1 files changed, 9 insertions, 1 deletions
diff --git a/.merlin b/.merlin
index 02420c4d..24226a91 100644
--- a/.merlin
+++ b/.merlin
@@ -1,7 +1,9 @@
-FLG -rectypes
+FLG -rectypes -thread
S config
B config
+S ide
+B ide
S lib
B lib
S intf
@@ -12,6 +14,8 @@ S kernel/byterun
B kernel/byterun
S library
B library
+S engine
+B engine
S pretyping
B pretyping
S interp
@@ -24,6 +28,8 @@ S printing
B printing
S parsing
B parsing
+S stm
+B stm
S toplevel
B toplevel
@@ -33,3 +39,5 @@ S tools/coqdoc
B tools/coqdoc
S dev
B dev
+
+PKG threads.posix