diff --git a/.hgignore b/.hgignore
--- a/.hgignore
+++ b/.hgignore
@@ -1,76 +1,77 @@
 syntax: glob
 
 afp-export-20??-??-??
 
 *.pyc
 *~
 .DS_Store
 
 thys/Tree-Automata/code/haskell/generated/Nat.hs
 thys/Tree-Automata/code/haskell/generated/Ta.hs
 thys/Tree-Automata/code/ml/generated/Ta.ML
 thys/Tree-Automata/code/ocaml/generated/Ta.ml
 
 thys/BinarySearchTree/BinaryTree_Code.ML
 thys/BinarySearchTree/BinaryTree_TacticStyle_Code.ML
 
 thys/CAVA_LTL_Modelchecker/code/examples/mulog/Mulog_Export.sml
 
 thys/ClockSynchInst/document/abs_distrib_mult.cvc
 thys/ClockSynchInst/document/abs_distrib_mult.ics
 thys/ClockSynchInst/document/abs_distrib_mult2.cvc
 thys/ClockSynchInst/document/accur_pres.cvc
 thys/ClockSynchInst/document/accur_pres.ics
 thys/ClockSynchInst/document/bound_prec_enh.cvc
 thys/ClockSynchInst/document/bound_prec_enh.ics
 thys/ClockSynchInst/document/bound_prec_enh4.cvc
 thys/ClockSynchInst/document/bound_prec_enh7.cvc
 
 thys/Depth-First-Search/dfs.ML
 
 thys/Well_Quasi_Orders/generated/
 
 thys/JinjaThreads/Execute/JVM_Execute2.ML
 thys/JinjaThreads/Execute/JWellForm.ML
 thys/JinjaThreads/Execute/J_Execute.ML
 thys/JinjaThreads/JVM_Execute2.ML
 thys/JinjaThreads/JWellForm.ML
 thys/JinjaThreads/J_Execute.ML
 
 thys/Vickrey_Clarke_Groves/VCG-withoutWrapper.scala
 
 thys/CAVA_LTL_Modelchecker/Nested_DFS/nested_dfs_hash.sml
 thys/CAVA_LTL_Modelchecker/code/CAVA_Export.sml
 
 thys/Collections/Examples/Autoref/nested_dfs.sml
 
 thys/Promela/Promela.sml
 
 thys/Formal_SSA/BraunSSA.ml
 
 thys/LTL_to_DRA/Code/LTL_to_DRA_Translator.sml
 
 thys/EdmondsKarp_Maxflow/evaluation/fofu-SML/Fofu_Export.sml
 
 thys/Refine_Imperative_HOL/benchmarks/Dijkstra/isabelle/dijkstra_export.sml
 thys/Refine_Imperative_HOL/benchmarks/Heapmap/isabelle/heapmap_export.sml
 thys/Refine_Imperative_HOL/benchmarks/NestedDFS/isabelle/NDFS_Benchmark_export.sml
 
 thys/SPARCv8/SparcModel_MMU/sparc_seq
 
 thys/Tree-Automata/code/haskell/generated/Array.hs
 thys/Tree-Automata/code/haskell/generated/Data_Bits.hs
 thys/Tree-Automata/code/haskell/generated/Natural.hs
 thys/Tree-Automata/code/haskell/generated/Uint32.hs
 
 thys/Verified_SAT_Based_AI_Planning/code/generated
 
 thys/Simplicial_complexes_and_boolean_functions/BDD/*.hs
 thys/Simplicial_complexes_and_boolean_functions/SMLBDD
 
 admin/py-bootstrap
 admin/venv
 
 tools/**.jar
 web/hugo
 out/
+admin/site