diff -r 078ad17eb934 -r a037f01aedab Admin/components/optional
--- a/Admin/components/optional	Fri May 07 16:45:49 2021 +0200
+++ b/Admin/components/optional	Fri May 07 16:49:08 2021 +0200
@@ -1,2 +1,2 @@
-#optional components that could impact build time significantly
+#optional components: somewhat experimental tools
 hol-light-bundle-0.5-126