+# prepend_line filename line
+#
+# Prepend a line to a file (this is better than appending, because it
+# works even when the original file isn't terminated with a newline).
+prepend_line ()
+{
+ $gf download "$1" "$tmpdir/file"
+ echo "$2" > "$tmpdir/file.1"
+ cat "$tmpdir/file.1" "$tmpdir/file" >> "$tmpdir/file.2"
+ $gf upload "$tmpdir/file.2" "$1"
+}
+