update updatehtml to git-add html files

martinescardo · Nov 21, 2024 · 88d7680 · 88d7680
1 parent 9ffd8ff
commit 88d7680
Showing 1 changed file with 1 addition and 0 deletions.
diff --git 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