forgot to actually use the certfile parameter.

diff --git a/scripts/rev_control/push_repo_upstream.sh b/scripts/rev_control/push_repo_upstream.sh
index 13e8ba0e0232e197b272da076b247cc6f7f3a30b..5b99f3b914af75af106cc98214de33f99417513e 100755 (executable)
--- a/scripts/rev_control/push_repo_upstream.sh
+++ b/scripts/rev_control/push_repo_upstream.sh
@@ -22,5 +22,5 @@ fi
 pushd "$dir"
 git fetch upstream
 git merge upstream/master
-git push origin master
+git push -i "$certfile" origin master
 popd