From ae731b2e2f31d4203f2e2765b4a0155ccf80cb6d Mon Sep 17 00:00:00 2001
From: Luke Naylor <l.naylor@sms.ed.ac.uk>
Date: Thu, 27 Jul 2023 19:51:32 +0100
Subject: [PATCH] Remove redundant sed script
---
filter_sage.sed | 23 -----------------------
1 file changed, 23 deletions(-)
delete mode 100755 filter_sage.sed
diff --git a/filter_sage.sed b/filter_sage.sed
deleted file mode 100755
index 7b59fe3..0000000
--- a/filter_sage.sed
+++ /dev/null
@@ -1,23 +0,0 @@
-#!/usr/bin/sed -f
-
-0,/^\\begin{sagesilent}/b nonsage
-/^\\end{sagesilent}/,/^\\begin{sagesilent}/b nonsage
-
-1 {
-:nonsage
- s/.*\\sage{\(.*\)}.*/# RENDERED TO LATEX: \1/p
- t end
- s/.*\\section{\(.*\)}.*/## SECTION \1 ##/
- T skip;
- h;s/\S/#/g;H;G;a
- p
- b end
-:skip
- s/.*\\subsection{\(.*\)}.*/# SUB SECTION \1 #/
- T end;
- h;s/\S/#/g;H;g;a
- p
- b end
-:end
- d
-}
--
GitLab