From f0cc9dcdc774e3cec4da757cb33715e73754de23 Mon Sep 17 00:00:00 2001
From: Giovanni Bussi <giovanni.bussi@gmail.com>
Date: Sun, 21 Jul 2019 18:44:29 +0200
Subject: [PATCH] added mirror for xdrfile lib on our github organization

---
 .travis/install.xdrfile | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/.travis/install.xdrfile b/.travis/install.xdrfile
index e30bb5a31..f095dad78 100755
--- a/.travis/install.xdrfile
+++ b/.travis/install.xdrfile
@@ -10,8 +10,10 @@ echo "installing xdrfile library"
 # xdrfile was removed from gromacs ftp
 # as a workaround I added a copy to people.sissa.it/~bussi/plumed
 # this complies with its license
+# wget people.sissa.it/~bussi/plumed/xdrfile-1.1.4.tar.gz
 
-wget people.sissa.it/~bussi/plumed/xdrfile-1.1.4.tar.gz
+# better to download from github, that should be even more reliable:
+wget https://github.com/plumed/other_packages/blob/master/xdrfile-1.1.4.tar.gz
 
 tar xzf xdrfile-1.1.4.tar.gz
 
-- 
GitLab