# HG changeset patch
# User wenzelm
# Date 1497273607 -7200
# Node ID 0a34bfc15e2c668c6278a22287fda1e8bf4f8c88
# Parent  f8899f6071ac9e6aef7396efabc121862df55cd7
obsolete;

diff -r f8899f6071ac -r 0a34bfc15e2c .hgignore
--- 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/