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

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

@ionchy how do you need js for this? how is the web the biggest standard, hugest thing yet you cannot make the iframe just be big enough with css. how. what is the web?

Sign in to participate in the conversation

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