Add a settings page and make Jerrin happy

1 files changed, 0 insertions, 17 deletions

diff --git a/main.js b/main.js
index ae7f1d3..3cf8d05 100644
--- a/main.js
+++ b/main.js
@@ -100,20 +100,3 @@ function parse_time(event)
 	if (document.getElementById("startobj").value && document.getElementById("endobj").value)
 		compute();
 }
-
-/* Change the users preferred theme. */
-function change_theme()
-{
-	const theme_switch = document.getElementById("page_theme");
-	const want = theme_switch.checked ? "dark" : "light";
-
-	document.documentElement.setAttribute("theme", want);
-	localStorage.setItem("theme", want);
-}
-
-/* Automatically select the users preferred theme */
-const theme = localStorage.getItem("theme");
-if (theme) {
-	document.documentElement.setAttribute("theme", theme);
-	document.getElementById("page_theme").checked = (theme == "dark");
-}