# HG changeset patch
# User wenzelm
# Date 1289940892 -3600
# Node ID bf8f92bdf6307f1edd875897eae2daf9a2114b75
# Parent  ffcff7509a499780979ec7f269188e86b8f997cd
init_component: require absolute path (when invoked by user scripts);

diff -r ffcff7509a49 -r bf8f92bdf630 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Tue Nov 16 21:48:14 2010 +0100
+++ b/lib/scripts/getsettings	Tue Nov 16 21:54:52 2010 +0100
@@ -91,6 +91,13 @@
 function init_component ()
 {
   local COMPONENT="$1"
+  case "$COMPONENT" in
+    /*) ;;
+    *)
+      echo >&2 "Absolute component path required: \"$COMPONENT\""
+      exit 2
+      ;;
+  esac
 
   if [ ! -d "$COMPONENT" ]; then
     echo >&2 "Bad Isabelle component: \"$COMPONENT\""