From 30d3515546cf244837c6340b6b87c5f51e68cbf4 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Tue, 17 Jan 2017 23:40:35 +0100
Subject: [location] Remove Loc.ghost.

Now it is a private field, locations are optional.
---
 .merlin | 2 ++
 1 file changed, 2 insertions(+)

(limited to '.merlin')

diff --git a/.merlin b/.merlin
index 5cae15f5f..5c8c73851 100644
--- a/.merlin
+++ b/.merlin
@@ -36,6 +36,8 @@ S toplevel
 B toplevel
 S vernac
 B vernac
+S plugins/ltac
+B plugins/ltac
 
 S tools
 B tools
-- 
cgit v1.2.3