--- a/.hgignore Mon Jun 12 11:41:54 2017 +0200
+++ b/.hgignore Mon Jun 12 15:20:07 2017 +0200
@@ -19,5 +19,4 @@
^src/Tools/jEdit/dist/
^src/Tools/VSCode/out/
^src/Tools/VSCode/extension/node_modules/
-^src/Tools/VSCode/extension/protocol.log
^Admin/jenkins/ci-extras/target/