mkslides
author nipkow
Mon, 31 Jul 2017 14:30:33 +0200
changeset 69882 f6d14918f41b
parent 69814 37690822a0f9
permissions -rwxr-xr-x
.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
69814
37690822a0f9 Revived exercise fundus
lammich <lammich@in.tum.de>
parents: 69809
diff changeset
     1
#!/bin/sh
37690822a0f9 Revived exercise fundus
lammich <lammich@in.tum.de>
parents: 69809
diff changeset
     2
37690822a0f9 Revived exercise fundus
lammich <lammich@in.tum.de>
parents: 69809
diff changeset
     3
if test $# -eq 0; then SESSIONS=Slides; else SESSIONS="$@"; fi
37690822a0f9 Revived exercise fundus
lammich <lammich@in.tum.de>
parents: 69809
diff changeset
     4
37690822a0f9 Revived exercise fundus
lammich <lammich@in.tum.de>
parents: 69809
diff changeset
     5
isabelle build -v -d . $SESSIONS