mkdir -p bin;
authorwenzelm
Wed Nov 05 19:40:50 1997 +0100 (1997-11-05)
changeset 417777f65eb64da4
parent 4176 84a0bfbd74e5
child 4178 e64ff1c1bc70
mkdir -p bin;
src/Tools/8bit/mk
     1.1 --- a/src/Tools/8bit/mk	Wed Nov 05 19:39:34 1997 +0100
     1.2 +++ b/src/Tools/8bit/mk	Wed Nov 05 19:40:50 1997 +0100
     1.3 @@ -2,10 +2,13 @@
     1.4  #
     1.5  # $Id$
     1.6  #
     1.7 -# mk - build 8bit.
     1.8 +# mk - build 8bit
     1.9  #
    1.10  # Assumes to be called with current directory 'Tools/8bit'
    1.11  
    1.12 -export ISABELLE8BIT=$(pwd)
    1.13 +export ISABELLE8BIT=$PWD
    1.14 +
    1.15 +mkdir -p bin
    1.16  touch Makefile
    1.17 +
    1.18  gmake