deploy: 7d5ae1a

ocsigen · Nov 3, 2023 · 1755381 · 1755381
1 parent 05ec96e
commit 1755381
Show file tree

Hide file tree

Showing 94 changed files with 1,148 additions and 60 deletions.
diff --git a/highlight.pack.js b/highlight.pack.js
diff --git a/index.html b/index.html
@@ -2,7 +2,7 @@
 <html xmlns="http://www.w3.org/1999/xhtml">
   <head>
     <title>index</title>
-    <link rel="stylesheet" href="./odoc.css"/>
+    <link rel="stylesheet" href="./odoc.support/odoc.css"/>
     <meta charset="utf-8"/>
     <meta name="viewport" content="width=device-width,initial-scale=1.0"/>
   </head>

diff --git a/ocsipersist-dbm/Ocsidbmtypes/.dune-keep b/ocsipersist-dbm/Ocsidbmtypes/.dune-keep