lib/browser/build
changeset 72982 adda33fdb5d0
parent 71373 201486ced92d
equal deleted inserted replaced
72981:c78d1dfc6571 72982:adda33fdb5d0
    61 then
    61 then
    62   echo >&2 "### Building graph browser ..."
    62   echo >&2 "### Building graph browser ..."
    63 
    63 
    64   rm -rf classes && mkdir classes
    64   rm -rf classes && mkdir classes
    65 
    65 
    66   isabelle_jdk javac -d classes -source 1.6 "${SOURCES[@]}" || \
    66   isabelle_jdk javac -d classes -source 7 "${SOURCES[@]}" || \
    67     fail "Failed to compile sources"
    67     fail "Failed to compile sources"
    68   isabelle_jdk jar cf "$(platform_path "$TARGET")" -C classes . ||
    68   isabelle_jdk jar cf "$(platform_path "$TARGET")" -C classes . ||
    69     fail "Failed to produce $TARGET"
    69     fail "Failed to produce $TARGET"
    70 
    70 
    71   rm -rf classes
    71   rm -rf classes