John J. Camilleri b73f033b08 Rewrite <a name=...> to <div id=...> to preserve page anchors in Pandoc

2018-12-05 16:11:33 +01:00

..

build-binary-dist.sh

build-binary-dist.sh: make it easy to choose which version of ghc to use

2018-12-01 15:53:27 +01:00

clean_html

Update clean_html to handle markdown sources too

2018-12-03 10:49:37 +01:00

gfmap

Final changes before the release of GF 3.9

2017-08-11 21:11:24 +02:00

template.html

Put GF logo on the right again

2018-12-03 15:27:55 +01:00

update_html

Rewrite <a name=...> to <div id=...> to preserve page anchors in Pandoc

2018-12-05 16:11:33 +01:00