# 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/