From 6028e10398896e89f965e35dee1935ec1140d518 Mon Sep 17 00:00:00 2001
From: Joris Van den Bossche <jorisvandenbossche@gmail.com>
Date: Wed, 14 Mar 2018 13:46:57 +0100
Subject: [PATCH] CI: builds docs on every commit

---
 ci/build_docs.sh | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/ci/build_docs.sh b/ci/build_docs.sh
index a038304fe0f7a..5de9e158bcdb6 100755
--- a/ci/build_docs.sh
+++ b/ci/build_docs.sh
@@ -10,11 +10,11 @@ echo "inside $0"
 
 git show --pretty="format:" --name-only HEAD~5.. --first-parent | grep -P "rst|txt|doc"
 
-if [ "$?" != "0" ]; then
-    echo "Skipping doc build, none were modified"
-    # nope, skip docs build
-    exit 0
-fi
+# if [ "$?" != "0" ]; then
+#     echo "Skipping doc build, none were modified"
+#     # nope, skip docs build
+#     exit 0
+# fi
 
 
 if [ "$DOC" ]; then