Build.rc.local

diff --git a/Build.rc.local.example b/Build.rc.local.example
new file mode 100644 (file)
index 0000000..495eaa7
--- /dev/null
+++ b/Build.rc.local.example
@@ -0,0 +1,12 @@
+# -*- sh -*-
+# -----------------------------------------------------------------------------
+# Additional configuration file for ./Build
+# -----------------------------------------------------------------------------
+#
+# Build.rc.local is purely optional. When it exists, it is evaluated
+# after Build.rc to allow overriding some configurations in Build.rc.
+#
+# Please note that it is unsafe to override some configurations,
+# namely "setPrefix" and "setPath", as they affect other variables in
+# a non-predictable way.
+#

diff --git a/Makefile b/Makefile
index 2260df74616ed32d1bec0fc1f4e77e83c28a1523..0e487ffb8c1ebf803917f55c8be5a37b52571c6f 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -14,12 +14,17 @@ clean:
        rm -f Build Build.tmp
 
 Build: $(SOURCES)
+# Concatenate the source files to $@.tmp.
        rm -f $@ $@.tmp
        for i in $(SOURCES); do \
                cat $$i >> $@.tmp; \
                echo >> $@.tmp; \
        done
-       head -q -n -1 $@.tmp > $@
+# Copy the content of $@.tmp to $@ except for the last line.
+       lines=`wc -l $@.tmp | awk '{print $$1}'` && \
+               lines=`expr $$lines - 1` && \
+               head -n $$lines $@.tmp > $@
+# Clean up.
        rm -f $@.tmp
        chmod a=rx $@
 

diff --git a/src/resource.bash b/src/resource.bash
index a05000658046b5f1b42bebafafb5dd092ff5a980..5ae60ef221d273659bc1cbd7ed76c3f414ae60a8 100644 (file)
--- a/src/resource.bash
+++ b/src/resource.bash
@@ -5,6 +5,10 @@ setBuildTarget "all"
 setDocDirectory "."
 setDocTarget "all"
 
-if [ -f "Build.rc" ]; then
+if [[ -f "Build.rc" ]]; then
     . "Build.rc"
 fi
+
+if [[ -f "Build.rc.local" ]]; then
+    . "Build.rc.local"
+fi