chore: remove website

This has been extracted to its own repository
leanprover · Dec 6, 2023 · d9c12fd · d9c12fd
1 parent 6a67a77
commit d9c12fd
Show file tree

Hide file tree

Showing 25 changed files with 0 additions and 1,035 deletions.
diff --git a/BlogContents.lean b/BlogContents.lean
diff --git a/BlogContents/Pages/Blog.lean b/BlogContents/Pages/Blog.lean
diff --git a/BlogContents/Pages/Contact.lean b/BlogContents/Pages/Contact.lean
diff --git a/BlogContents/Pages/Front.lean b/BlogContents/Pages/Front.lean
diff --git a/BlogContents/Pages/Links.lean b/BlogContents/Pages/Links.lean
diff --git a/BlogContents/Pages/Mission.lean b/BlogContents/Pages/Mission.lean
diff --git a/BlogContents/Pages/Roadmap.lean b/BlogContents/Pages/Roadmap.lean
diff --git a/BlogContents/Pages/Team.lean b/BlogContents/Pages/Team.lean
diff --git a/BlogContents/Posts/AnExcellentPost.lean b/BlogContents/Posts/AnExcellentPost.lean
diff --git a/BlogContents/Posts/AnotherPost.lean b/BlogContents/Posts/AnotherPost.lean
diff --git a/DemoBlog.lean b/DemoBlog.lean
diff --git a/lakefile.lean b/lakefile.lean
@@ -22,13 +22,3 @@ lean_exe «leandoc» where
   -- `runFrontend`) at the expense of increased binary size on Linux.
   -- Remove this line if you do not need such functionality.
   supportInterpreter := true
-
-lean_lib BlogContents where
-
-@[default_target]
-lean_exe «demoblog» where
-  root := `DemoBlog
-  -- Enables the use of the Lean interpreter by the executable (e.g.,
-  -- `runFrontend`) at the expense of increased binary size on Linux.
-  -- Remove this line if you do not need such functionality.
-  supportInterpreter := true
diff --git a/src/leandoc/LeanDoc/Doc/Lsp.lean b/src/leandoc/LeanDoc/Doc/Lsp.lean
@@ -36,8 +36,6 @@ defmethod Syntax.lspRange (text : FileMap) (s : Syntax) : Option Lsp.Range :=
   | _ => none
 
 
-
-
 open Lean.Lsp in
 instance : FromJson DocumentHighlightKind where
   fromJson?

diff --git a/static/bindings.js b/static/bindings.js