Why do I need an internet connection to compile my GitHub Pages static site locally?

Let's see if I can insert an HTML page in another HTML page without JS...

Like just let me \include{agda/Girard.agda} pls that's all I need

iframes it is
how do I make it as tall as it needs to be to not have a scrollbar

Follow

CW: Javascript 

  let details = document.querySelectorAll("details");
details.forEach((detail) => {
detail.hasBeenExpanded = false;
detail.addEventListener("toggle", () => {
if (!detail.hasBeenExpanded) {
detail.hasBeenExpanded = true;
let iframe = detail.getElementsByTagName("iframe")[0];
iframe.style.height = iframe.contentDocument.body.scrollHeight + 30 + "px";
}
});
});

re: CW: Javascript 

for some reason 30px is exactly the amount I need to add. I don't know why and I will not question it

tbh I really don't mind using Javascript on my blog for little things like this where I'm just fetching some elements and setting fields
It's a short piece of code that I've written myself and that's easy to understand, and probably easier to decipher than some cursed CSS incantations when I come back a year later
But jQuery? no. nuh uh. I'm not loading up a whole giant JS file even it's minimized just so I can $ select something. the abstractions are overkill and don't look all that much shorter than the plain JS anyway

Sign in to participate in the conversation
types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.