diff --git a/updatehtml b/updatehtml index 207cc03c4..df6487a8f 100755 --- a/updatehtml +++ b/updatehtml @@ -10,6 +10,7 @@ rm -rf html agda --highlight-occurrences --html AllModulesIndex.lagda rm -f ~/martinescardo.github.io/TypeTopology/*.html # do not delete Agda.css, as it is a modified version mv html/*.html ~/martinescardo.github.io/TypeTopology/ +git add ~/martinescardo.github.io/TypeTopology/*.html chmod a+r ~/martinescardo.github.io/TypeTopology/*.html # Now create copies for files that have been moved to other places