Skip to content

Commit

Permalink
Update locations for new infrastructure
Browse files Browse the repository at this point in the history
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...
  • Loading branch information
maximedenes committed Jun 14, 2019
1 parent 93f53d6 commit fe0442b
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion update_opam_git.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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

0 comments on commit fe0442b

Please sign in to comment.