f6fe00db5c
It's time to start preparing for a version of redo that doesn't work unless we build it first (because it will rely on C modules, and eventually be rewritten in C altogether). To get rolling, remove the old-style symlinks to the main programs, and rename those programs from redo-*.py to redo/cmd_*.py. We'll also move all library functions into the redo/ dir, which is a more python-style naming convention. Previously, install.do was generating wrappers for installing in /usr/bin, which extend sys.path and then import+run the right file. This made "installed" redo work quite differently from running redo inside its source tree. Instead, let's always generate the wrappers in bin/, and not make anything executable except those wrappers. Since we're generating wrappers anyway, let's actually auto-detect the right version of python for the running system; distros can't seem to agree on what to call their python2 binaries (sigh). We'll fill in the right #! shebang lines. Since we're doing that, we can stop using /usr/bin/env, which will a) make things slightly faster, and b) let us use "python -S", which tells python not to load a bunch of extra crap we're not using, thus improving startup times. Annoyingly, we now have to build redo using minimal/do, then run the tests using bin/redo. To make this less annoying, we add a toplevel ./do script that knows the right steps, and a Makefile (whee!) for people who are used to typing 'make' and 'make test' and 'make clean'.
25 lines
688 B
JavaScript
25 lines
688 B
JavaScript
'use strict';
|
|
|
|
async function fetchCode(e, lang, src) {
|
|
const resp = await fetch(src);
|
|
let t = await resp.text();
|
|
if (lang) t = hljs.highlight(lang, t).value;
|
|
e.innerHTML = t;
|
|
}
|
|
|
|
function fetchAndHighlightAll() {
|
|
const el = document.getElementsByTagName('code');
|
|
for (const e of el) {
|
|
const src = e.getAttribute('src');
|
|
if (!src) continue;
|
|
const lang = e.getAttribute('lang');
|
|
const title = document.createElement('b');
|
|
title.innerText = src;
|
|
title.style.textAlign = 'center';
|
|
title.style.display = 'block';
|
|
e.parentElement.insertBefore(title, e);
|
|
fetchCode(e, lang, src);
|
|
}
|
|
}
|
|
|
|
setTimeout(fetchAndHighlightAll, 0);
|