aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Thomas Refis <thomas.refis@gmail.com>2014-04-03 02:48:41 +0900
committerGravatar Pierre Boutillier <pierre.boutillier@ens-lyon.org>2014-04-03 14:50:49 +0200
commit48af6d1418282323b9fff0e789fed9478c064434 (patch)
treeccd3b54cf0d95a36a9b966356b7e04db43fadcc0
parent49a2f8411fc69c9cdffc776a25fcb521aab7de74 (diff)
Clean up the .merlin
I added a .merlin in ide/ who inherits everything from the root .merlin and also adds the dependency to lablgtk, which I removed from the root file. These way people not working on that part of the code won't get bothered if they don't have that package. I removed the S/B entry for plugins which was useless, indeed there is no ML file in that directory and merlin doesn't scan the subdirectories recursively (as you know). I also removed the S/B entry for checker since most of the files of this directory are also present in kernel and that was the cause of a lot errors on merlin's side (think "inconsistent assumptions"). On top of that, no part of the tree depends on checker (I back that assertion by a grep of the *.d files of the tree) so these lines in the .merlin were actually useless. The only part of the tree where you need to know what's in checker/ is when you are working in checker/ itself, but since merlin automatically adds the directory of the file under edition in its source and load paths nothing else is needed. There might still be problems after this patch, but they should be less of them. Considering my poor knowledge of the codebase there might be other conflicts I have missed.
-rw-r--r--.merlin10
-rw-r--r--ide/.merlin6
2 files changed, 6 insertions, 10 deletions
diff --git a/.merlin b/.merlin
index f0f0c31c9..02420c4d8 100644
--- a/.merlin
+++ b/.merlin
@@ -26,20 +26,10 @@ S parsing
B parsing
S toplevel
B toplevel
-S plugins
-B plugins
-PKG lablgtk2.sourceview2
-S ide
-B ide
-S ide/utils
-B ide/utils
S tools
B tools
S tools/coqdoc
B tools/coqdoc
S dev
B dev
-
-S checker
-B checker
diff --git a/ide/.merlin b/ide/.merlin
new file mode 100644
index 000000000..3f3d9d275
--- /dev/null
+++ b/ide/.merlin
@@ -0,0 +1,6 @@
+PKG lablgtk2.sourceview2
+
+S utils
+B utils
+
+REC