#
# Doesn't fit perfectly in this file, but this is the best place to make it
# available everywhere.
+#
+# If DEBUG is set to a non empty value additional debug output is printed.
function source_config() {
# Path to the file to source and its local counterpart.
local source_file=$1/$2/$3.$4