1 files changed, 1 insertions, 1 deletions

diff --git a/Makefile b/Makefile
index b57cb54..fc30a49 100644
--- a/Makefile
+++ b/Makefile
@@ -31,7 +31,7 @@ $(NAME).pdf: $(NAME).dtx
         mv TMP/*.pdf samples/
         mv $(texsamplesout)-tei.xml samples/
         @ echo "Build the documentation of $(NAME)..."
-        $(CMP) --shell-escape -recorder -interaction=batchmode $(NAME).dtx >/dev/null
+        $(CMP) --shell-escape --recorder --interaction=batchmode $(NAME).dtx >/dev/null
         biber $(NAME) >/dev/null
         if [ -f $(NAME).glo ]; then makeindex -q -s gglo.ist -o $(NAME).gls $(NAME).glo; fi
         if [ -f $(NAME).idx ]; then makeindex -q -s gind.ist -o $(NAME).ind $(NAME).idx; fi