diff -r aa3581fc685c -r 923f9c9f56c5 .hgignore
--- a/.hgignore	Tue Feb 12 14:43:45 2019 +0100
+++ b/.hgignore	Tue Feb 12 16:11:54 2019 +0100
@@ -32,3 +32,4 @@
 ^doc/_build
 ^doc/js_api/
 test-results.xml
+ve