-
Notifications
You must be signed in to change notification settings - Fork 0
/
header.html
52 lines (51 loc) · 2.16 KB
/
header.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
<!-- General -->
<meta charset="UTF-8">
<meta name="viewport" content="width=device-width, initial-scale=1">
<!-- Favicon -->
<link rel="apple-touch-icon" sizes="180x180" href="/favicon/apple-touch-icon.png">
<link rel="icon" type="image/png" sizes="32x32" href="/favicon/favicon-32x32.png">
<link rel="icon" type="image/png" sizes="16x16" href="/favicon/favicon-16x16.png">
<link rel="manifest" href="/favicon/site.webmanifest">
<!-- Fonts -->
<link rel="preconnect" href="https://fonts.googleapis.com">
<link rel="preconnect" href="https://fonts.gstatic.com" crossorigin>
<link href="https://fonts.googleapis.com/css2?family=Commissioner:wght@300;400;500;600&family=Inconsolata:wght@400;700&display=swap" rel="stylesheet">
<!-- Includes -->
<script>
if (document.documentElement.lang === "en") {
$(function(){
$("#navbar").load("/en/navbar.html");
$("#footer").load("/en/footer.html");
});
}else{
$(function(){
$("#navbar").load("/lv/navbar.html");
$("#footer").load("/lv/footer.html");
});
}
// code to handle copy-pasting on the website
document.addEventListener('copy', function (event) {
const selection = window.getSelection();
if (selection.isCollapsed) {
return; // default action OK
}
const fragment = selection.getRangeAt(0).cloneContents();
const katexs = fragment.querySelectorAll('.katex');
if (katexs.length === 0) {
return; // default action OK
}
katexs.forEach (function (element) {
const texSource = element.querySelector('annotation');
if (texSource) {
element.replaceWith(texSource);
texSource.innerHTML = '$' + texSource.innerHTML + '$';
}
});
fragment.querySelectorAll('.katex-display annotation').forEach (function (element) {
element.innerHTML = '$' + element.innerHTML + '$';
})
event.clipboardData.setData('text/plain', fragment.textContent);
event.clipboardData.setData('text/html', selection.getRangeAt(0).cloneContents());
event.preventDefault();
});
</script>