(whoops, just noticed that my patch also edits debian/ant.properties - it still works, but i guess you'll want to fix that.)
-- GPG: 4096R/5FBBDBCE -- To UNSUBSCRIBE, email to debian-bugs-dist-requ...@lists.debian.org with a subject of "unsubscribe". Trouble? Contact listmas...@lists.debian.org
