--- a/.hgtags	Fri Jul 20 13:17:08 2018 +0200
+++ b/.hgtags	Fri Jul 20 13:17:08 2018 +0200
@@ -3,3 +3,4 @@
 7ceac963fe2441a0ef9522bb814f4216646e1abb 0.1.2
 7ceac963fe2441a0ef9522bb814f4216646e1abb 0.1.2
 3b6ac2a2be6493f132cd964e2cd7b04b56109808 0.1.2
+5be82b23c046df82c4d171752c07f1f6f67c15cb 0.1.3
changeset 20	1f1d69342248
parent 14	f55890b180cd
child 23	4e799a208d50