diff options
| author | Dieter Plaetinck <dieter@plaetinck.be> | 2010-08-07 22:31:31 +0200 |
|---|---|---|
| committer | Dieter Plaetinck <dieter@plaetinck.be> | 2010-08-07 22:31:31 +0200 |
| commit | 4a52b78e4287ac29f4c32f611c7c5e54cba67c3f (patch) | |
| tree | 3e8ea63d05012d2aa744d52702b3793e3179250f /make-doc.sh | |
| parent | 622e61271f4f13a14909dc50286098a2f9a6b814 (diff) | |
turn code markup into a syntax that mediawiki understands
<pre><code></code></pre> puts '<code></code>' in the rendered block
<code><pre></pre></code> and <pre></pre> seem to be work fine, so we use
the latter.
<code></code> seems not understood by mediawiki at all. at least it's
rendered incorrectly.
fixes FS#19640
Diffstat (limited to 'make-doc.sh')
| -rwxr-xr-x | make-doc.sh | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/make-doc.sh b/make-doc.sh index 2bfd4c9..4e6c5a2 100755 --- a/make-doc.sh +++ b/make-doc.sh @@ -7,6 +7,10 @@ do echo $i # convert markdown to html, convert html links to wiki ones. cat $i | markdown | sed 's|<a href="\([^"]*\)"[^>]*>\([^<]*\)</a>|[\1 \2]|g' > $i.html + # turn code markup into a syntax that mediawiki understands + sed -i 's#<pre><code>#<pre>#g' $i.html + sed -i 's#</code></pre>#</pre>#g' $i.html + done echo "adding special wiki thingies..." |