remove unnecessary index.html

tamarin-prover · Jul 17, 2023 · 1a1ebf0 · 1a1ebf0
1 parent e06746b
commit 1a1ebf0
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/deploy.sh b/deploy.sh
@@ -38,8 +38,7 @@ do
     cp -r $x $CHECKOUT/$BRANCH
 done
 cp tex/tamarin-manual.pdf $CHECKOUT/$BRANCH/tex/tamarin-manual.pdf
-cp index.html $CHECKOUT/$BRANCH/index.html
-# put index.html also to root directory
+# put index.html to root directory
 cp index.html $CHECKOUT/index.html
 
 # If there are no changes to the compiled book (e.g. this is a README update) then just bail.