File tree Expand file tree Collapse file tree 4 files changed +4
-3
lines changed
Expand file tree Collapse file tree 4 files changed +4
-3
lines changed Original file line number Diff line number Diff line change @@ -13,7 +13,7 @@ test: test/Tests.agda
1313test/Tests.agda : test/Main.hs test/typed/* .agda test/untyped/* .agda
1414 cabal test
1515
16- html : test
16+ html : test
1717 make -C test html
1818
1919clean :
Original file line number Diff line number Diff line change 8181.tab-content { height : 100% ; }
8282.tabs__tab { height : 100% ; }
8383embed { height : 100% ; width : 100% ; }
84+ .code { white-space : pre-wrap; }
Original file line number Diff line number Diff line change 22MAIN =Tests
33.PHONY : html clean
44
5- html :
5+ html :
66 @echo == Generating HTML ==
77 mkdir -p html/ && cp Agda.css html/
88 -cabal run -- agda2lambox --html --css=Agda.css $(MAIN ) .agda
Original file line number Diff line number Diff line change @@ -26,7 +26,7 @@ for f in $BUILD_DIR/**/**; do
2626 echo " \`\`\` " >> $mdFn
2727
2828 targetHtml=" $f " .html
29- pandoc --quiet -M document-css=false - i " $mdFn " -o " $targetHtml " -s --highlight-style=tango
29+ pandoc --quiet -i " $mdFn " -o " $targetHtml " --highlight-style=tango
3030done
3131
3232mkdir -p " $AGDA_HTML_DIR /$BUILD_DIR "
You can’t perform that action at this time.
0 commit comments