From 6cec568e452f66c9358888a3a358fdc822c6590d Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sat, 5 Jan 2019 18:39:35 +0000 Subject: [PATCH] Removed local output directory. --- Core_DOM/ROOT | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Core_DOM/ROOT b/Core_DOM/ROOT index 1b1a730..f4591ac 100644 --- a/Core_DOM/ROOT +++ b/Core_DOM/ROOT @@ -1,7 +1,7 @@ chapter AFP session "Core_DOM-devel" (AFP) = "HOL-Library" + - options [timeout = 4800, document = pdf, document_variants="document:outline=/proof,/ML",document_output=output] + options [timeout = 4800, document = pdf, document_variants="document:outline=/proof,/ML"] theories Core_DOM Core_DOM_Tests