Be compatible with shells of Ubuntu 14.04

lib/git/tools.sh

@@ -23,6 +23,7 @@ git_remove_history() {
       return
   fi
   # Remove all paths passed as arguments from the history of the repo
+  local files
   files=("$@")
   $_git_cmd filter-branch --index-filter "$_git_cmd rm -rf --cached --ignore-unmatch ${files[*]}" HEAD
   # Remove the temporary history git-filter-branch otherwise leaves behind for a long time
@@ -142,4 +143,4 @@ git_branch_delete_all() {
 
 commit_docs() {
   git commit -m "Update README / Documentation [ci skip]"
-}
+}