# HG changeset patch # User wenzelm # Date 1621435480 -7200 # Node ID 6ddbb74a52c9bc4c3538f0f5d25e989468384445 # Parent e78c8a1f03fb3342a45aeb5713015266256669b8 unused; diff -r e78c8a1f03fb -r 6ddbb74a52c9 src/Doc/System/document/build --- a/src/Doc/System/document/build Wed May 19 16:41:32 2021 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -#!/usr/bin/env bash - -set -e - -FORMAT="$1" -VARIANT="$2" - -"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" - diff -r e78c8a1f03fb -r 6ddbb74a52c9 src/Doc/Typeclass_Hierarchy/document/build --- a/src/Doc/Typeclass_Hierarchy/document/build Wed May 19 16:41:32 2021 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -#!/usr/bin/env bash - -set -e - -FORMAT="$1" -VARIANT="$2" - -"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" -