Update html_header.html

spinkney · Jan 24, 2022 · d343c47 · d343c47
1 parent dc0bd60
commit d343c47
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/pretty/css/html_header.html b/pretty/css/html_header.html
@@ -15,7 +15,7 @@
 		$mathjax
 		<link href="$relpath^$stylesheet" rel="stylesheet" type="text/css" />
 		$extrastylesheet
-		<link rel="stylesheet" href="$relpath^sean-theme.css">
+		<!-- <link rel="stylesheet" href="$relpath^sean-theme.css">
 		<script src="$relpath^highlight.min.js"></script>
 		<script>
 	$(function() {
@@ -24,7 +24,7 @@
 		  $node.html("<pre><code class='stan'>" + 
 					 $node.text()+"</code></pre>");
 					 hljs.highlightAll(node);
-	});
+	}); -->
 });
 	</script>
 	</head>