diff options
| author | Enrico Tassi | 2020-09-11 14:55:07 +0200 |
|---|---|---|
| committer | Jim Fehrle | 2020-09-24 13:04:56 -0700 |
| commit | 6c5608acde0a9bbaa3e2f7317b9b5cf2de2699cd (patch) | |
| tree | e4245480c346e8985bc5a62679f06359c9365622 /ide | |
| parent | e0b8b4684eaf76f897ac708ffddbb8e4977ac754 (diff) | |
fix ide/.merlin
Diffstat (limited to 'ide')
| -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 |