--- a/.hgignore Tue May 31 12:24:43 2016 +0200 +++ b/.hgignore Tue May 31 18:31:33 2016 +0200 @@ -20,3 +20,4 @@ ^doc/.*\.pdf ^doc/.*\.ps ^src/Tools/jEdit/dist/ +^Admin/jenkins/ci-extras/target/