New function source_debug().

Prints given arguments if $DEBUG is non empty. At the moment only used by
source_config().

diff --git a/shell/env b/shell/env
index be55b4e863f1b808a3b2186aa20b5722d88b2a0e..e30b2722e8de10547a182ff83dbeac2052202bc1 100644 (file)
--- a/shell/env
+++ b/shell/env
@@ -1,6 +1,17 @@
 # Configuration file for environment related options for all shells.
 
 
+# Helper function to print debug information if $DEBUG is not empty.
+#
+# Doesn't fit perfectly in this file, but this is the best place to make it
+# available everywhere.
+function source_debug() {
+    if [ x$DEBUG != x ]; then
+        echo $@
+    fi
+}
+
+
 # Use UTF-8 encoding in the terminal.
 LC_ALL=en_US.UTF-8
 LANG=$LC_ALL
@@ -88,24 +99,18 @@ function source_config() {
     local source_file_local=$1/$3.local
 
     # Additional debug output.
-    if [ x$DEBUG != x ]; then
-        echo "source_config(): checking if $source_file exists"
-        echo "source_config(): checking if $source_file_local exists"
-    fi
+    source_debug "source_config(): checking if $source_file exists"
+    source_debug "source_config(): checking if $source_file_local exists"
 
     # If the file does exist then source it.
     if [ -f $source_file ]; then
-        if [ x$DEBUG != x ]; then
-            echo "source_config(): sourcing $source_file"
-        fi
+        source_debug "source_config(): sourcing $source_file"
         source $source_file
 
     # Otherwise load the .local file if it exists and .local files are
     # allowed.
     elif [ -f $source_file_local -a x$5 != xnolocal ]; then
-        if [ x$DEBUG != x ]; then
-            echo "source_config(): sourcing $source_file_local"
-        fi
+        source_debug "source_config(): sourcing $source_file_local"
         source $source_file_local
     fi
 }