diff -r 3e076cc76c89 -r aff3a6ca254b .hgtags
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/.hgtags	Tue Jul 30 23:56:32 2019 +0200
@@ -0,0 +1,1 @@
+3e076cc76c899c993b9e151416de6b772b43d27b v0.13