From 707ccc2e782b359725308ebd8cbcc3f904a1b0d9 Mon Sep 17 00:00:00 2001 From: Thomas Letan Date: Fri, 14 Feb 2020 08:06:52 +0100 Subject: Provide an index page for write-ups with more value --- .gitignore | 7 +++--- Makefile | 4 +-- plugins/site-prefix.lua | 4 +++ site/index.html | 2 +- site/posts.org | 66 +++++++++++++++++++++++++++++++++++++++++++++++++ site/posts/index.html | 22 ----------------- site/style/main.css | 17 +++++++++++++ 7 files changed, 94 insertions(+), 28 deletions(-) create mode 100644 site/posts.org delete mode 100644 site/posts/index.html diff --git a/.gitignore b/.gitignore index 6c3c797..fe3275d 100644 --- a/.gitignore +++ b/.gitignore @@ -8,12 +8,13 @@ build/ *.html~ # begin generated files +site/posts.html +site/posts/DiscoveringCommonLisp.html site/posts/ExtensibleTypeSafeErrorHandling.html site/posts/MonadTransformers.html -site/posts/DiscoveringCommonLisp.html -site/posts/Ltac101.html -site/posts/RewritingInCoq.html site/posts/StronglySpecifiedFunctionsProgram.html site/posts/MiniHTTPServer.html site/posts/StronglySpecifiedFunctions.html +site/posts/RewritingInCoq.html +site/posts/Ltac101.html # begin generated files diff --git a/Makefile b/Makefile index 3d96f5e..807cb27 100644 --- a/Makefile +++ b/Makefile @@ -1,5 +1,5 @@ -ORG_POSTS := $(wildcard site/posts/*.org) -COQ_POSTS := $(wildcard site/posts/*.v) +ORG_POSTS := $(shell find site/ -name "*.org") +COQ_POSTS := $(shell find site/ -name "*.v") POSTS := $(ORG_POSTS:.org=.html) $(COQ_POSTS:.v=.html) COQCARGS := -async-proofs-cache force diff --git a/plugins/site-prefix.lua b/plugins/site-prefix.lua index e64f839..6c7f12a 100644 --- a/plugins/site-prefix.lua +++ b/plugins/site-prefix.lua @@ -15,7 +15,11 @@ index, link = next(links) while index do href = HTML.get_attribute(link, "href") + if href then + -- remove prefix sometimes introduced by org + href = Regex.replace(href, "^file://", "") + -- Check if URL starts with a leading "/" if Regex.match(href, "^/") then -- Remove leading slashes diff --git a/site/index.html b/site/index.html index 0fa4132..7d08c4a 100644 --- a/site/index.html +++ b/site/index.html @@ -24,7 +24,7 @@