diff --git a/doc/build-manuals.sh b/doc/build-manuals.sh
index ee63e0d148b9a5c68ecf8a947eb5d0f7f6b74de7..3f330a4ea60ce67b3216d7da404d3af2b932f8f6 100755
--- a/doc/build-manuals.sh
+++ b/doc/build-manuals.sh
@@ -63,8 +63,12 @@ build () {
         echo "######### $1 failed"
         exit 1
     fi
-    # extract extension, add suffix, re-append extension
-    MANUAL=${2%.*}-$3.${2##*.}
+    if [ "$NO_SUFFIX" == "yes" ] ; then
+        MANUAL=$2
+    else
+        # extract extension, add suffix, re-append extension
+        MANUAL=${2%.*}-$3.${2##*.}
+    fi
     cp -f $1 manuals/$MANUAL
     echo "##### $MANUAL copied"
 
@@ -112,7 +116,7 @@ else
 fi
 
 # Sanity check: version differences between Frama-C, ACSL and E-ACSL
-FAIL = 0
+FAIL=0
 if [ "$ACSL_SUFFIX" != "$EACSL_SUFFIX" ]; then
     echo "WARNING: different versions for ACSL and E-ACSL manuals: $ACSL_SUFFIX versus $EACSL_SUFFIX"
     FAIL=1