Update build

Remove PR_ from the published version.
cplusplus · Oct 21, 2024 · da55d5d · da55d5d
1 parent ee55d0e
commit da55d5d
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/tools/build/build b/tools/build/build
@@ -77,7 +77,7 @@ if [ -z "$version" ]; then
   usage "no document version specified"
 fi
 
-version=PR_${version%/*}
+version=${version%/*}
 
 ################################################################################
 # Build the document.