moved from dev to prod

2022-11-14 10:05:42 +01:00
parent ac142715b0
commit 43d589aa9b
1364 changed files with 27705 additions and 6101 deletions
--- a/tools/highwire/html/help/menu.css
+++ b/tools/highwire/html/help/menu.css
@@ -0,0 +1,2 @@
+dt      { white-space:nowrap }
+dt.open { background-color:#1E90FF }