# HG changeset patch
# User wenzelm
# Date 1667733638 -3600
# Node ID 98cfe33db5a75f878ba7552510287073d1ebac4a
# Parent  01109e16cee836a0435636e0a87fd1d86f57ae66
further attempts to confine dotnet to $ISABELLE_HOME_USER;

diff -r 01109e16cee8 -r 98cfe33db5a7 src/Pure/Tools/dotnet_setup.scala
--- a/src/Pure/Tools/dotnet_setup.scala	Sun Nov 06 12:11:13 2022 +0100
+++ b/src/Pure/Tools/dotnet_setup.scala	Sun Nov 06 12:20:38 2022 +0100
@@ -96,6 +96,7 @@
 fi
 
 DOTNET_CLI_TELEMETRY_OPTOUT="true"
+DOTNET_CLI_HOME="$(platform_path "$ISABELLE_HOME_USER/dotnet")"
 """)
 
         File.write(component_dir + Path.explode("README"),