lib/Tools/make
author wenzelm
Fri, 01 Sep 2000 17:50:36 +0200
changeset 9788 df671fa2562a
parent 7795 111d2a65e1c6
child 10511 efb3428c9879
permissions -rwxr-xr-x
GPLed; more robust handling of spaces in args / file names;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3007
e5efa177ee0c removed -norc;
wenzelm
parents: 2593
diff changeset
     1
#!/bin/bash
2437
63249c1c544a Isabelle make utility;
wenzelm
parents:
diff changeset
     2
#
63249c1c544a Isabelle make utility;
wenzelm
parents:
diff changeset
     3
# $Id$
9788
wenzelm
parents: 7795
diff changeset
     4
# Author: Markus Wenzel, TU Muenchen
wenzelm
parents: 7795
diff changeset
     5
# License: GPL (GNU GENERAL PUBLIC LICENSE)
2437
63249c1c544a Isabelle make utility;
wenzelm
parents:
diff changeset
     6
#
63249c1c544a Isabelle make utility;
wenzelm
parents:
diff changeset
     7
# DESCRIPTION: Isabelle make utility
63249c1c544a Isabelle make utility;
wenzelm
parents:
diff changeset
     8
63249c1c544a Isabelle make utility;
wenzelm
parents:
diff changeset
     9
9788
wenzelm
parents: 7795
diff changeset
    10
PRG=$(basename "$0")
2437
63249c1c544a Isabelle make utility;
wenzelm
parents:
diff changeset
    11
63249c1c544a Isabelle make utility;
wenzelm
parents:
diff changeset
    12
function usage()
63249c1c544a Isabelle make utility;
wenzelm
parents:
diff changeset
    13
{
63249c1c544a Isabelle make utility;
wenzelm
parents:
diff changeset
    14
  echo
63249c1c544a Isabelle make utility;
wenzelm
parents:
diff changeset
    15
  echo "Usage: $PRG [ARGS ...]"
63249c1c544a Isabelle make utility;
wenzelm
parents:
diff changeset
    16
  echo
7795
111d2a65e1c6 tuned usage;
wenzelm
parents: 3007
diff changeset
    17
  echo "  Compile the logic in current directory using IsaMakefile."
2437
63249c1c544a Isabelle make utility;
wenzelm
parents:
diff changeset
    18
  echo "  ARGS are directly passed to the system make program."
63249c1c544a Isabelle make utility;
wenzelm
parents:
diff changeset
    19
  echo
63249c1c544a Isabelle make utility;
wenzelm
parents:
diff changeset
    20
  exit 1
63249c1c544a Isabelle make utility;
wenzelm
parents:
diff changeset
    21
}
63249c1c544a Isabelle make utility;
wenzelm
parents:
diff changeset
    22
63249c1c544a Isabelle make utility;
wenzelm
parents:
diff changeset
    23
63249c1c544a Isabelle make utility;
wenzelm
parents:
diff changeset
    24
## main
63249c1c544a Isabelle make utility;
wenzelm
parents:
diff changeset
    25
63249c1c544a Isabelle make utility;
wenzelm
parents:
diff changeset
    26
[ "$1" = "-?" ] && usage
63249c1c544a Isabelle make utility;
wenzelm
parents:
diff changeset
    27
63249c1c544a Isabelle make utility;
wenzelm
parents:
diff changeset
    28
exec make -f IsaMakefile "$@"