Adaptation Makefile pour git.

Makefile

@@ -1,8 +1,29 @@
+# Ce Makefile est là purement par commodité : la vraie fonctionnalité
+# est dans les scripts TML et les hooks du dépôt git ; rien dans la
+# procédure de mise à jour du site web ne devrait exiger de passer par
+# make.
+
+
+.PHONY: rebuild install
+
+
+gitdir = /users/staffs/tuteurs/www.git
+originurl = $(shell git config --get remote.origin.url)
+
+
 rebuild:
 	/users/staffs/tuteurs/share/tml/bin/rebuild .
 
-install:
+
-	cvstuteurs commit
+# C'est un hook déclenché par git push qui fait l'installation du site
-	su-tuteurs cvstuteurs update -d /users/staffs/tuteurs/www
+# web. Ici, on essaie juste de voir si on est en local sur clipper
-	su-tuteurs /users/staffs/tuteurs/share/tml/bin/rebuild /users/staffs/tuteurs/www
+# (auquel cas on n'a peut-être pas le droit d'écrire chez tuteurs, mais
+# su-tuteurs nous le donnera). Sinon c'est probablement qu'on a cloné
+# par ssh (de chez soi ou de clipper), et on devrait savoir pousser.
+
+install:
+	case ${originurl} in \
+	  ${gitdir} ) /users/staffs/tuteurs/bin/sg-tuteurs git push ;; \
+	  * ) git push ;; \
+	esac