diff -r 0d3eb5129582 -r 535a232e6014 .hgtags
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/.hgtags	Tue Jul 30 23:56:30 2019 +0200
@@ -0,0 +1,1 @@
+0d3eb5129582878ca800b5ab3241d5f2907a3eb9 v0.13