From 5b89ababd527fdb34090241d2bac620e4c8354a3 Mon Sep 17 00:00:00 2001
From: baldurk <baldurk@baldurk.org>
Date: Sat, 18 Aug 2018 16:44:05 +0100
Subject: [PATCH] Prefer make.sh for building docs as htmlhelp is removed from
 Makefile

* Also it's more flexible in locating necessary tools like sphinx-build or
  python
---
 util/buildscripts/scripts/compile_win32.sh | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/util/buildscripts/scripts/compile_win32.sh b/util/buildscripts/scripts/compile_win32.sh
index 8133051a5..4664ff5b3 100755
--- a/util/buildscripts/scripts/compile_win32.sh
+++ b/util/buildscripts/scripts/compile_win32.sh
@@ -25,8 +25,8 @@ fi
 
 # Step into the docs folder and build
 pushd docs
-make clean
-make htmlhelp > /tmp/sphinx.log
+./make.sh clean
+./make.sh htmlhelp > /tmp/sphinx.log
 
 if [ $? -ne 0 ]; then
 	$ERROR_SCRIPT /tmp/sphinx.log