proper initialization of settings: avoid accidental intrusion from parent process environment;
authorwenzelm
Sun, 12 Jan 2025 21:39:57 +0100
changeset 81797 d7113296c541
parent 81796 88c172ebffdd
child 81798 a0ecb9d06664
proper initialization of settings: avoid accidental intrusion from parent process environment;
src/Tools/Find_Facts/etc/settings
--- a/src/Tools/Find_Facts/etc/settings	Sun Jan 12 21:38:38 2025 +0100
+++ b/src/Tools/Find_Facts/etc/settings	Sun Jan 12 21:39:57 2025 +0100
@@ -4,5 +4,6 @@
 FIND_FACTS_WEB="$ISABELLE_HOME_USER/find_facts/web"
 
 SOLR_DATA="$ISABELLE_HOME_USER/find_facts/solr"
+SOLR_COMPONENTS=""
 
 ISABELLE_TOOLS="$ISABELLE_TOOLS:$FIND_FACTS_HOME/Tools"