From f755da76634fb524e64d057384d0201146623279 Mon Sep 17 00:00:00 2001
From: Pete Jemian <prjemian@gmail.com>
Date: Thu, 23 Jan 2020 09:16:17 -0600
Subject: [PATCH] MNT #720 one more instance

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

diff --git a/jenkins_build b/jenkins_build
index 7fede891a7..f7a0ddf8a6 100755
--- a/jenkins_build
+++ b/jenkins_build
@@ -14,7 +14,7 @@ make builddir
 cd build
 make
 
-( cd ../impatient-guide && rm -rf _build && make latexpdf && make html )
+( cd ../impatient-guide && rm -rf _build && make latexpdf LATEXOPTS="--interaction=nonstopmode" && make html )
 
 # publish
 if test "${job_name}" = "master branch"; then