Admin/lib/Tools/makedist_cygwin
changeset 50838 ad959a8b951e
parent 50834 506342881c33
child 50839 9cc70b273e90
equal deleted inserted replaced
50837:db0012672241 50838:ad959a8b951e
    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:\tmp' \
    57   --root "$(cygpath -w "$TARGET")" \
    57   --root "$(cygpath -w "$TARGET")" \
    58   --packages libgmp3,perl,python,rlwrap \
    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
    62 
    62 
    63 
    63