diff options
| -rw-r--r-- | ide/.merlin.in | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/ide/.merlin.in b/ide/.merlin.in index b8d7953833..50816ae3f5 100644 --- a/ide/.merlin.in +++ b/ide/.merlin.in @@ -1,8 +1,10 @@ PKG unix laglgtk3 lablgtk3-sourceview3 -S utils -B utils -S protocol -B protocol +S coqide/utils +B coqide/utils +S coqide/protocol +B coqide/protocol +S coqide/ +B coqide/ REC |