diff -r 4244e4b5e124 -r a81828f24172 .hgignore
--- a/.hgignore	Wed Apr 07 21:33:01 2021 +0200
+++ b/.hgignore	Mon Mar 22 14:47:06 2021 +0100
@@ -13,8 +13,6 @@
 src/HOL/SPARK/Examples/Sqrt/sqrt/isqrt.prv
 src/HOL/SPARK/Manual/simple_greatest_common_divisor/g_c_d.prv
 
-etc/settings                        #does NOT work !?!
-
 syntax: regexp
 
 #cygwin: requires different 'components' and 'settings'--------\