Closed williamdemeo closed 3 years ago
add generate-html and generate-tex files to automatically make html and tex documentation
create new monolithic reference manual in the doc directory (note that the makefile for this doesn't work yet, but it compiles with
pdflatex agda-algebras
from within the doc directory, after invoking the command generate-tex from the top (agda-algebras) directory).
doc
generate-tex
agda-algebras
plus many other improvements
add generate-html and generate-tex files to automatically make html and tex documentation
create new monolithic reference manual in the doc directory (note that the makefile for this doesn't work yet, but it compiles with
from within the
doc
directory, after invoking the commandgenerate-tex
from the top (agda-algebras
) directory).plus many other improvements