Skip to content

Commit

Permalink
feat: add Lean logo
Browse files Browse the repository at this point in the history
  • Loading branch information
david-christiansen committed Oct 19, 2024
1 parent b7c739e commit 45e80f0
Show file tree
Hide file tree
Showing 4 changed files with 100 additions and 9 deletions.
7 changes: 4 additions & 3 deletions Main.lean
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,8 @@ where
config := {
extraFiles := [("static", "static")],
extraCss := ["/static/colors.css", "/static/theme.css", "/static/print.css", "/static/fonts/source-serif/source-serif-text.css", "/static/fonts/source-code-pro/source-code-pro.css", "/static/katex/katex.min.css"],
extraJs := ["/static/katex/katex.min.js", "/static/math.js", "/static/print.js"]
emitTeX := false
emitHtmlSingle := true -- for proofreading
extraJs := ["/static/katex/katex.min.js", "/static/math.js", "/static/print.js"],
emitTeX := false,
emitHtmlSingle := true, -- for proofreading
logo := some "/static/lean_logo.svg"
}
2 changes: 1 addition & 1 deletion lake-manifest.json
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@
"type": "git",
"subDir": null,
"scope": "",
"rev": "4c7f449c296461794d5260dd044f2629e53e8532",
"rev": "625054ef9e53e3b9167252f59fd55589aa56e196",
"name": "verso",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
Expand Down
90 changes: 90 additions & 0 deletions static/lean_logo.svg
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
10 changes: 5 additions & 5 deletions static/theme.css
Original file line number Diff line number Diff line change
Expand Up @@ -105,7 +105,7 @@ figcaption {

/** Temporary measures until the real release **/

body::before {
main::before {
content: 'Preview Release';
position: fixed;
top: 0;
Expand All @@ -122,13 +122,13 @@ body::before {
background-color: var(--lean-compl-yellow);
font-family: var(--verso-structure-font-family);
font-size: large;
z-index: -1; /* don't show under marginal notes*/
}

span.TODO, .marginalia .note {
z-index: -2;
}

#print {
display: none;
}

#top-menu {

}

0 comments on commit 45e80f0

Please sign in to comment.