# HG changeset patch
# User wenzelm
# Date 1494092569 -7200
# Node ID 92028ab1c3d7b547cecf555d4765f9b828ec6351
# Parent  4847ca570454a7f998a7d9671decf38d37c6f782
obsolete;

diff -r 4847ca570454 -r 92028ab1c3d7 .hgignore
--- a/.hgignore	Sat May 06 19:23:33 2017 +0200
+++ b/.hgignore	Sat May 06 19:42:49 2017 +0200
@@ -15,13 +15,9 @@
 ^contrib
 ^heaps/
 ^browser_info/
-^doc/.*\.dvi
-^doc/.*\.eps
 ^doc/.*\.pdf
-^doc/.*\.ps
 ^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/
-^stats/