From 178d6e9793117cc17560dd595cd66754d13109d7 Mon Sep 17 00:00:00 2001
From: Victor Lin <13424970+victorlin@users.noreply.github.com>
Date: Mon, 14 Oct 2024 17:50:18 -0700
Subject: [PATCH] Allow BUILDDIR to be set from environment

Follow-up to "Allow BUILDDIR to be set from environment" (2f2f98b8)
where I forgot the existence of the make.bat file.
---
 make.bat | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/make.bat b/make.bat
index fa71760f..fcf21072 100644
--- a/make.bat
+++ b/make.bat
@@ -7,8 +7,10 @@ REM Command file for Sphinx documentation
 if "%SPHINXBUILD%" == "" (
 	set SPHINXBUILD=sphinx-build
 )
+if "%BUILDDIR%" == "" (
+	set SPHINXBUILD=build
+)
 set SOURCEDIR=src
-set BUILDDIR=build
 
 if "%1" == "" goto help