From 5c20c3eeed4aad9043b84169bc4ea648ec4b4e80 Mon Sep 17 00:00:00 2001
From: Luke Naylor <l.naylor@sms.ed.ac.uk>
Date: Thu, 27 Apr 2023 00:34:03 +0100
Subject: [PATCH] Box up generated comments in sage filter
---
filter_sage.sed | 11 +++++------
1 file changed, 5 insertions(+), 6 deletions(-)
diff --git a/filter_sage.sed b/filter_sage.sed
index 676fa19..8184701 100755
--- a/filter_sage.sed
+++ b/filter_sage.sed
@@ -2,12 +2,11 @@
0,/^\\begin{sagesilent}/d
/^\\end{sagesilent}/,/^\\begin{sagesilent}/{
- s;.*\\sage{\(.*\)}.*;\n# RENDERED TO LATEX: \1 #;p
- t underline
- d
-:underline
- s;^\n;;
+ s;.*\\sage{\(.*\)}.*;# RENDERED TO LATEX: \1 #;
+ T end; h
s;\S;#;g
- s;$;\n;p
+ H; G; a
+ p
+:end
d
}
--
GitLab