Admin/lib/Tools/makedist_cygwin
changeset 50839 9cc70b273e90
parent 50838 ad959a8b951e
child 50887 1cadc8a8b377
equal deleted inserted replaced
50838:ad959a8b951e 50839:9cc70b273e90
    51 
    51 
    52 # install
    52 # install
    53 
    53 
    54 "$TARGET/isabelle/cygwin.exe" \
    54 "$TARGET/isabelle/cygwin.exe" \
    55   --site "$CYGWIN_MIRROR" --no-verify \
    55   --site "$CYGWIN_MIRROR" --no-verify \
    56   --local-package-dir 'C:\tmp' \
    56   --local-package-dir 'C:\temp' \
    57   --root "$(cygpath -w "$TARGET")" \
    57   --root "$(cygpath -w "$TARGET")" \
    58   --packages libgmp3,make,perl,python,rlwrap,vim \
    58   --packages libgmp3,make,perl,python,rlwrap,vim \
    59   --no-shortcuts --no-startmenu --no-desktop --quiet-mode
    59   --no-shortcuts --no-startmenu --no-desktop --quiet-mode
    60 
    60 
    61 [ "$?" = 0 -a -e "$TARGET/etc" ] || exit 2
    61 [ "$?" = 0 -a -e "$TARGET/etc" ] || exit 2