From ba2ff73b62b9c06383f9a83e80e08b7ac1dcdd83 Mon Sep 17 00:00:00 2001
From: Marc Mezzarobba <marc@mezzarobba.net>
Date: Sun, 20 Sep 2009 13:24:46 +0200
Subject: [PATCH] Adaptation Makefile pour git.

---
 Makefile | 29 +++++++++++++++++++++++++----
 1 file changed, 25 insertions(+), 4 deletions(-)

diff --git a/Makefile b/Makefile
index a4300f9..65f2487 100644
--- a/Makefile
+++ b/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
-	su-tuteurs cvstuteurs update -d /users/staffs/tuteurs/www
-	su-tuteurs /users/staffs/tuteurs/share/tml/bin/rebuild /users/staffs/tuteurs/www
+
+# C'est un hook déclenché par git push qui fait l'installation du site
+# web. Ici, on essaie juste de voir si on est en local sur clipper
+# (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