From 8f5b89f12226380e6ceb7e3d7d5b50b4a0a763fe Mon Sep 17 00:00:00 2001
From: Anthony Scemama <scemama@irsamc.ups-tlse.fr>
Date: Fri, 14 Dec 2018 10:16:13 +0100
Subject: [PATCH] configure

---
 configure | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/configure b/configure
index f080fed0..dba83b69 100755
--- a/configure
+++ b/configure
@@ -207,7 +207,7 @@ EOF
             chmod +x "${QP_ROOT}"/external/opam_installer.sh
             rm -f ${QP_ROOT}/bin/opam
 
-            if [[ ${TRAVIS} = true ]] ; then
+            if [[ -n ${TRAVIS} ]] ; then
                 # Special commands for Travis CI
                 export OPAMROOT=${HOME}/.opam
                 cat << EOF | sh ${QP_ROOT}/external/opam_installer.sh --no-backup