Add strip_prefix function.

This function can be used to remove a given prefix from a string.

diff --git a/lib/tools.in b/lib/tools.in
index b180950789c60ead1def01525e69dca8c78279e2..4ca438f05e8dc17fc7d44537e66145609a0d1dc4 100644 (file)
--- a/lib/tools.in
+++ b/lib/tools.in
@@ -97,3 +97,11 @@ function starts_with() {
        # Is it equal to $2?
        [ "$head" = "$2" ]
 }
+
+# Strip the prefix $2 from $1. Assumes that $1 actually starts with $1.
+# The result is put on stdout.
+function strip_prefix() {
+       # Strip the first ${#2} (the length of $2) characters from $1.
+       # tail -c +N means start at the Nth byte, 1-based, so we add 1.
+       echo $1 | tail -c +$((${#2}+1))
+}