aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMatej Kosik2016-10-28 11:48:46 +0200
committerMatej Kosik2016-11-03 09:26:43 +0100
commit9c52d25ac0badc5ec6eb0eb897219e607c362e83 (patch)
treeda5fdc825cf46b32b6fe8519ad46b2b710f4b0bd
parent19a2dd5cfbd72defe932656a65ab9da9f4ac9d1e (diff)
updating ".merlin" file
-rw-r--r--.merlin2
1 files changed, 2 insertions, 0 deletions
diff --git a/.merlin b/.merlin
index 7ae6422335..7279a098e9 100644
--- a/.merlin
+++ b/.merlin
@@ -1,5 +1,7 @@
FLG -rectypes -thread
+S ltac
+B ltac
S config
B config
S lib