on master help sign in
Minor fix to latex sphinx build configuration.

Build was failing locally with \textlambda not being found. Added new package for fix. Changed name of generated pdf to match project name, and removed second PDF file in list. This hopefuly will make RTD build again... Update PDF of tutorial in source repository.

commitbc8926c1b9d73d8d70a85c64498c063e97bb1c59 authorJan de Muijnck-Hughes <jan.deMuijnck-Hughes@glasgow.ac.uk> dateTue 10 Mar 2020, 14:12 (7 years ago) parentbbd0f28
2 files changed+3−2
docs/conf.py+3−2 idris-tutorial.pdf
docs/conf.py+3−2
@@ -251,6 +251,7 @@ latex_elements = {
251251# Additional stuff for the LaTeX preamble.
252252'preamble': r'''
253253\usepackage{lmodern}
254+\usepackage{textalpha}
254255\usepackage[T1]{fontenc}
255256\usepackage[utf8x]{inputenc}
256257\usepackage{titlesec}
@@ -300,8 +301,8 @@ latex_elements = {
300301# (source start file, target name, title,
301302# author, documentclass [howto, manual, or own class]).
302303latex_documents = [
303− ('index', 'idris-documentation-complete.tex', u'Documentation for the Idris Language', u'The Idris Community', 'report'),
304− ('tutorial/index', 'idris-tutorial.tex', u'The Idris Tutorial', u'The Idris Community', 'howto'),
304+ (master_doc, 'idris.tex', u'Documentation for the Idris Language', u'The Idris Community', 'report')
305+ , ('tutorial/index', 'idris-tutorial.tex', u'The Idris Tutorial', u'The Idris Community', 'howto'),
305306]
306307
307308
idris-tutorial.pdf

Binary file not shown.