From fe0442bf5e6f2541517265539aab8d9f42045b4a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maxime=20D=C3=A9n=C3=A8s?= <maxime.denes@inria.fr>
Date: Fri, 14 Jun 2019 12:37:01 +0200
Subject: [PATCH] Update locations for new infrastructure

I doubt this script should be part of the repo. As of today, it is
served, and in case of self-upgrade, things will derail quickly...
---
 update_opam_git.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/update_opam_git.sh b/update_opam_git.sh
index 0800e41eff..050c398d62 100755
--- a/update_opam_git.sh
+++ b/update_opam_git.sh
@@ -8,5 +8,5 @@ REMOTE=$(git rev-parse @{u})
 
 if [ $LOCAL != $REMOTE ]; then
     git pull
-    PATH="/usr/local/bin:$PATH" make COQWEB=/srv/coq-www/www all
+    PATH="/usr/local/bin:$PATH" make COQWEB=/var/deploy/coq-www all
 fi