diff --git a/build_tools/circle/build_doc.sh b/build_tools/circle/build_doc.sh
index fb8e7da5b66b15748d83b1c5e0aee866253cda8b..a08359d93fe2c7fabe6207d4d49a159ba6eb0130 100755
--- a/build_tools/circle/build_doc.sh
+++ b/build_tools/circle/build_doc.sh
@@ -74,10 +74,8 @@ fi
 
 if [[ "$CIRCLE_BRANCH" =~ ^master$|^[0-9]+\.[0-9]+\.X$ && -z "$CI_PULL_REQUEST" ]]
 then
-    # dist generates the pdf doc and adds the pdf to the website
-    # nonstopmode is used to prevent CI timeout when the LaTeX
-    # compilation fails
-    MAKE_TARGET="dist LATEXMKOPTS=-interaction=nonstopmode"
+    # PDF linked into HTML
+    MAKE_TARGET="dist LATEXMKOPTS=-halt-on-error"
 elif [[ "$build_type" =~ ^QUICK ]]
 then
 	MAKE_TARGET=html-noplot