From fbcd79febd3625787fb2253043311b9f2d96bb48 Mon Sep 17 00:00:00 2001
From: Jentsch <d@jentsch.berlin>
Date: Mon, 29 Apr 2019 09:54:54 +0200
Subject: [PATCH] Fix smooth scrolling on index doc page

Somehow the animation with Javascript was broken, as it scrolled up the
top and than jupped the actual target.
Since ~70% of all browser support this with pure CSS today, this should
be good enough for this minor feature.

The 'local' class was only used within JavaScript so it was dropped.
---
 docs/css/default.css |  1 +
 docs/js/index.js     | 17 -----------------
 2 files changed, 1 insertion(+), 17 deletions(-)

diff --git a/docs/css/default.css b/docs/css/default.css
index 5f1928bfd313..285b7eb52f70 100644
--- a/docs/css/default.css
+++ b/docs/css/default.css
@@ -6,6 +6,7 @@
 
 html, body {
     box-sizing: border-box;
+    scroll-behavior: smooth;
 }
 
 *, *:before, *:after {
diff --git a/docs/js/index.js b/docs/js/index.js
index 029a9e703efd..493be83e2292 100644
--- a/docs/js/index.js
+++ b/docs/js/index.js
@@ -1,21 +1,4 @@
 $(document).ready(function() {
     window.sr = ScrollReveal();
     sr.reveal(".scala-logo-container",  { duration: 2000, delay: 100, mobile: false });
-
-    var hostname = new RegExp(location.host);
-    $('a').each(function(){
-        var url = $(this).attr("href");
-        if (hostname.test(url) || url.slice(0, 1) == "#")
-            $(this).addClass('local');
-    });
-
-    $("a").on('click', function(event) {
-        if ($(this).hasClass("local") && this.hash != "") {
-            event.preventDefault();
-            var hash = this.hash;
-            $('html, body').animate({ scrollTop: $(hash).offset().top }, 800, function() {
-                window.location.hash = hash;
-            });
-        }
-    });
 });