default document_build (lualatex);
authorwenzelm
Wed, 19 May 2021 11:48:35 +0200
changeset 73995 3e44f8c3f059
parent 73994 d701bd96e323
child 73996 c46ff0efa1ce
default document_build (lualatex);
src/Doc/Main/document/build
src/Doc/ROOT
--- a/src/Doc/Main/document/build	Wed May 19 11:18:38 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-#!/usr/bin/env bash
-
-set -e
-
-FORMAT="$1"
-VARIANT="$2"
-
-isabelle latex -o "$FORMAT"
-isabelle latex -o "$FORMAT"
-
--- a/src/Doc/ROOT	Wed May 19 11:18:38 2021 +0200
+++ b/src/Doc/ROOT	Wed May 19 11:48:35 2021 +0200
@@ -326,13 +326,11 @@
     "root.tex"
 
 session Main (doc) in "Main" = HOL +
-  options [document_build = "build", document_variants = "main"]
+  options [document_variants = "main"]
   theories Main_Doc
   document_files (in "..")
-    "prepare_document"
     "pdfsetup.sty"
   document_files
-    "build"
     "root.tex"
 
 session Nitpick (doc) in "Nitpick" = Pure +