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 16:53:30 +0100
commita4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch)
tree26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /.merlin
parent164c6861860e6b52818c031f901ffeff91fca16a (diff)
Imported Upstream version 8.6upstream/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