diff --git a/filter_sage.sed b/filter_sage.sed deleted file mode 100755 index 7b59fe38d26df073cc2e11d9b0194d08a268ffd8..0000000000000000000000000000000000000000 --- 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 -}