--- a/.hgignore Tue May 31 14:56:51 2016 +0200 +++ b/.hgignore Tue May 31 21:06:46 2016 +0200 @@ -20,3 +20,4 @@ ^doc/.*\.pdf ^doc/.*\.ps ^src/Tools/jEdit/dist/ +^Admin/jenkins/ci-extras/target/