src/Tools/8bit/mk
author wenzelm
Fri, 16 Jul 1999 22:25:07 +0200
changeset 7025 afbd8241797b
parent 4177 77f65eb64da4
permissions -rwxr-xr-x
tuned dest_lexicon;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4175
06774cd43054 *** empty log message ***
oheimb
parents:
diff changeset
     1
#!/bin/bash
06774cd43054 *** empty log message ***
oheimb
parents:
diff changeset
     2
#
06774cd43054 *** empty log message ***
oheimb
parents:
diff changeset
     3
# $Id$
06774cd43054 *** empty log message ***
oheimb
parents:
diff changeset
     4
#
4177
77f65eb64da4 mkdir -p bin;
wenzelm
parents: 4175
diff changeset
     5
# mk - build 8bit
4175
06774cd43054 *** empty log message ***
oheimb
parents:
diff changeset
     6
#
06774cd43054 *** empty log message ***
oheimb
parents:
diff changeset
     7
# Assumes to be called with current directory 'Tools/8bit'
06774cd43054 *** empty log message ***
oheimb
parents:
diff changeset
     8
4177
77f65eb64da4 mkdir -p bin;
wenzelm
parents: 4175
diff changeset
     9
export ISABELLE8BIT=$PWD
77f65eb64da4 mkdir -p bin;
wenzelm
parents: 4175
diff changeset
    10
77f65eb64da4 mkdir -p bin;
wenzelm
parents: 4175
diff changeset
    11
mkdir -p bin
4175
06774cd43054 *** empty log message ***
oheimb
parents:
diff changeset
    12
touch Makefile
4177
77f65eb64da4 mkdir -p bin;
wenzelm
parents: 4175
diff changeset
    13
4175
06774cd43054 *** empty log message ***
oheimb
parents:
diff changeset
    14
gmake