diff -r 662b5d5b1b70 -r 9ed8788a1a4e java/ant/tip.sh
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/java/ant/tip.sh	Fri Apr 03 16:32:36 2020 +0200
@@ -0,0 +1,2 @@
+#!/bin/sh
+hg id | cut -c1-12