This allows deploying the develop version of the manual onto the web page (I think)
Why? To have the develop version of the manual as easily accessible as the state-of-the-art manual. I think there might be as many people working with tamarin in develop as with master.
How does it work? deploy.sh checksout the branch gh-pages in a temporary folder $CHECKOUT, compiles the current work copy and copys it into $CHECKOUT. This PR changes the script so it copies it into $CHECKOUT/$BRANCH for $BRANCH the current workdir's branch. Moreover, index.html is prepared to prepend master respectively develop to the hrefs.
Known problems I do not know if this works. :D I tested locally and can confirm that compilation and copying succeeds and creates the appropriate structure. Pushing fails with iv undefined, which makes sense because travis has to do it. I think this is the simplest way to do it, but I don't quite know how travis works, so I need a reviewer familiar with the CI setup to look into it and maybe test it when there's not much user traffic.
This allows deploying the develop version of the manual onto the web page (I think)
Why? To have the develop version of the manual as easily accessible as the state-of-the-art manual. I think there might be as many people working with tamarin in
develop
as withmaster
.How does it work? deploy.sh checksout the branch
gh-pages
in a temporary folder $CHECKOUT, compiles the current work copy and copys it into $CHECKOUT. This PR changes the script so it copies it into$CHECKOUT/$BRANCH
for $BRANCH the current workdir's branch. Moreover,index.html
is prepared to prependmaster
respectivelydevelop
to the hrefs.Known problems I do not know if this works. :D I tested locally and can confirm that compilation and copying succeeds and creates the appropriate structure. Pushing fails with
iv undefined
, which makes sense because travis has to do it. I think this is the simplest way to do it, but I don't quite know how travis works, so I need a reviewer familiar with the CI setup to look into it and maybe test it when there's not much user traffic.