BrowserSecurity
/
Core_DOM-dev
Archivováno
rozštěpen z afp-mirror/Core_DOM
1
0
Rozštěpit 0
Zdrojový kód Úkoly Požadavky na natažení Vydání Wiki Aktivita

Enabled document generation.

This commit is contained in:
Achim D. Brucker 2020-04-16 23:31:15 +01:00
rodič 7563d9696e
revize 080f4db810
3 změnil soubory, kde provedl 5 přidání a 2 odebrání
Zobrazit statistiky Stáhněte soubor záplaty Stáhněte rozdílový soubor Rozbalit všechny soubory Sbalit všechny soubory

2
.gitignore vendorováno Normal file
Zobrazit soubor

@ -0,0 +1,2 @@
output

3
Core_DOM/Core_DOM/ROOT
Zobrazit soubor

@ -1,7 +1,7 @@
chapter AFP
session "Core_DOM" (AFP) = "HOL-Library" +
options [timeout = 1200]
options [timeout = 1200, document = pdf, document_variants="document:outline=/proof,/ML",document_output=output]
directories
"common"
"common/classes"
@ -18,3 +18,4 @@ session "Core_DOM" (AFP) = "HOL-Library" +
document_files (in "document")
"root.tex"
"root.bib"

2
Core_DOM/Core_SC_DOM/ROOT
Zobrazit soubor

@ -1,7 +1,7 @@
chapter AFP
session "Core_SC_DOM" (AFP) = "HOL-Library" +
options [timeout = 1200]
options [timeout = 1200, document = pdf, document_variants="document:outline=/proof,/ML",document_output=output]
directories
"common"
"common/classes"