src/Doc/Corec/document/build
author wenzelm
Wed, 12 Feb 2020 21:18:04 +0100
changeset 71440 8b0b8b9ea653
parent 62739 628c97d39627
permissions -rwxr-xr-x
afford newer Mercurial version, just before odd problems in 4.0 and 4.1;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62739
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
     1
#!/usr/bin/env bash
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
     2
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
     3
set -e
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
     4
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
     5
FORMAT="$1"
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
     6
VARIANT="$2"
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
     7
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
     8
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
     9