diff options
author | Oskar Vigren <oskar@vig.ren> | 2019-11-04 18:58:19 +0100 |
---|---|---|
committer | Gustav Eek <gustav.eek@fripost.org> | 2020-01-06 13:31:44 +0100 |
commit | 82016f6624dae1e61cf3cacba6a32540b1e3fa4e (patch) | |
tree | 87b824357a78ddea840ec28fd8af506154bc9049 /sed | |
parent | 8a489485dfd72788fd18728fd7c12b9c16053954 (diff) |
Remove unrelated pages for laboration
Diffstat (limited to 'sed')
-rw-r--r-- | sed/latex.sed | 18 |
1 files changed, 0 insertions, 18 deletions
diff --git a/sed/latex.sed b/sed/latex.sed deleted file mode 100644 index 1c46d3e..0000000 --- a/sed/latex.sed +++ /dev/null @@ -1,18 +0,0 @@ -#!/bin/sed -# -# Prepare for ODT -# -# This should be used after the markdown filter -/^\[\[!meta/,/^\]\]/ { - s/^\[\[!meta/---/ - s/^\]\]/.../ - s/ *\(.*\)="\(.*\)"/\1: \2/ -} - -/^\[\[!tag/ d -/^\[\[!toc/ d -/^\*\*InnehÄll\*\*$/ d - -s/DNS/\\textsc{dns}/ -s/ISBN/\\textsc{isbn}/ - |