Remove accidentally created dist folder

main
Elnu 1 year ago
parent d488b99765
commit b4a4a3f38a

3
.gitignore vendored

@ -1,2 +1,3 @@
/target /target
.direnv .direnv
dist

34
dist/index.html vendored

@ -1,34 +0,0 @@
<!DOCTYPE html><html lang="en"><head>
<meta charset="UTF-8">
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<title>dyesub-tool</title>
</head>
<body>
<script>(function () {
var protocol = window.location.protocol === 'https:' ? 'wss:' : 'ws:';
var url = protocol + '//' + window.location.host + '/_trunk/ws';
var poll_interval = 5000;
var reload_upon_connect = () => {
window.setTimeout(
() => {
// when we successfully reconnect, we'll force a
// reload (since we presumably lost connection to
// trunk due to it being killed, so it will have
// rebuilt on restart)
var ws = new WebSocket(url);
ws.onopen = () => window.location.reload();
ws.onclose = reload_upon_connect;
},
poll_interval);
};
var ws = new WebSocket(url);
ws.onmessage = (ev) => {
const msg = JSON.parse(ev.data);
if (msg.reload) {
window.location.reload();
}
};
ws.onclose = reload_upon_connect;
})()
</script></body></html>

@ -1,3 +0,0 @@
layout.json
output.svg
dist
Loading…
Cancel
Save