src/Tools/jEdit/makedist
changeset 34414 de921b3cb263
parent 34413 10cdbba5af89
child 34419 30e49efdd4e3
equal deleted inserted replaced
34413:10cdbba5af89 34414:de921b3cb263
     9 SUPER=$(cd "$THIS/.."; pwd)
     9 SUPER=$(cd "$THIS/.."; pwd)
    10 
    10 
    11 
    11 
    12 ## diagnostics
    12 ## diagnostics
    13 
    13 
    14 JEDIT_HOME="/home/isajedit/jedit-orig/4.3pre15"
    14 JEDIT_HOME="/home/isajedit/jedit-orig/4.3pre16"
    15 SCALA_HOME="/home/scala/current"
    15 SCALA_HOME="/home/scala/current"
    16 
    16 
    17 function usage()
    17 function usage()
    18 {
    18 {
    19   echo
    19   echo