src/Tools/8bit/mk
author wenzelm
Sun, 15 Oct 2000 19:50:35 +0200
changeset 10220 2a726de6e124
parent 4177 77f65eb64da4
permissions -rwxr-xr-x
proper symbol markup with \isamath, \isatext; support sub/super scripts:
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