diff --git a/.github/workflows/build.sh b/.github/workflows/build.sh index 8df3cc459c4..4713fa00e49 100755 --- a/.github/workflows/build.sh +++ b/.github/workflows/build.sh @@ -37,6 +37,7 @@ else fi mdbook build -d "$dest_dir" +sed -i '/./../../theme/redbox.js/d' ./../../theme/redbox.js if [ -f "$dest_dir/pandoc/pdf/comprehensive-rust.pdf" ]; then mv "$dest_dir/pandoc/pdf/comprehensive-rust.pdf" "$dest_dir/html/" fi