diff --git a/doc/build-manuals.sh b/doc/build-manuals.sh index 725ae1c670b36d9f33b091d199cb851cfd55c332..fccfa8c2403f068cc84747a34d36d4c7fa7ff7d1 100755 --- a/doc/build-manuals.sh +++ b/doc/build-manuals.sh @@ -46,7 +46,7 @@ build () { MANUAL=${2%.*}-$3.${2##*.} cp -f $1 manuals/$MANUAL echo "##### $MANUAL copied" - ln -srf manuals/$MANUAL manuals/$2 + } EACSL_DOC=../src/plugins/e-acsl/doc