Merge pull request #19 from odersky/add-banner

avoid header duplication 3nd attempt
odersky · Apr 12, 2024 · 87eb084 · 87eb084
2 parents d1f8935 + ca85898
commit 87eb084
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/_includes/header.html b/_includes/header.html
@@ -1,5 +1,5 @@
 <header class="site-header" role="banner">
-    <div class="wrapper" style="background-image: url('https://github.com/odersky/misc/blob/main/scala-stairs.png?raw=true'); height: 300px; background-size: cover; background-position: center;">
+    <div class="wrapper" style="background-image: url('https://github.com/odersky/misc/blob/main/scala-stairs.png?raw=true'); height: 200px; background-size: cover; background-position: center;">
         <a class="site-title" rel="author" href="{{ "/" | relative_url }}">{{ site.title | escape }}</a>
         <nav class="site-nav">
             <input type="checkbox" id="nav-trigger" class="nav-trigger" />