Push changes to repo description file

diff --git a/git-push-public b/git-push-public
index 4b57b9783f355e317ae95184d6ba6e195c214d03..39a89049c6a3057c1f9f287538544230cb8d540a 100755 (executable)
--- a/git-push-public
+++ b/git-push-public
@@ -23,6 +23,7 @@ push_repo()
     fi
     echo "-- syncing $repo"
     git --git-dir=$repo push --mirror $PUBLICSERVER:$PUBLICBASE/$repo
+    rsync -a $repo/description $PUBLICSERVER:$PUBLICBASE/$repo/description
 }
 
 ## MAIN ##