lib/Tools/testdir
author wenzelm
Fri, 07 Mar 1997 11:48:46 +0100
changeset 2754 59bd96046ad6
parent 2477 ff44d0e1953a
permissions -rwxr-xr-x
moved settings comment to build;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2477
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
     1
#!/bin/bash -norc
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
     2
#
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
     3
# $Id$
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
     4
#
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
     5
# DESCRIPTION: use dir without committing into database
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
     6
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
     7
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
     8
PRG=$(basename $0)
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
     9
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
    10
function usage()
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
    11
{
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
    12
  echo
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
    13
  echo "Usage: $PRG LOGIC DIR"
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
    14
  echo
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
    15
  echo "  Use dir without committing into database (FIXME ISABELLE_HTML)."
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
    16
  echo
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
    17
  exit 1
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
    18
}
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
    19
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
    20
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
    21
## args
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
    22
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
    23
[ $# -ne 2 ] && usage
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
    24
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
    25
LOGIC="$1"; shift
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
    26
DIR="$1"; shift
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
    27
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
    28
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
    29
## main
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
    30
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
    31
exec $ISABELLE \
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
    32
  -e "make_html := $ISABELLE_HTML;" \
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
    33
  -e "exit_use_dir\"$DIR\"; quit();" \
ff44d0e1953a testdir: use dir without committing into database;
wenzelm
parents:
diff changeset
    34
  -rq $LOGIC