Admin/lib/Tools/makedist_cygwin
changeset 58780 1f8c0da85664
parent 57389 eb96243a25c5
child 60005 e1d8c5099bef
equal deleted inserted replaced
58779:aeba9ae93dd8 58780:1f8c0da85664
    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:\temp' \
    56   --local-package-dir 'C:\temp' \
    57   --root "$(cygpath -w "$TARGET")" \
    57   --root "$(cygpath -w "$TARGET")" \
    58   --packages libgmp3,perl,perl_vendor,python,rlwrap,unzip,vim \
    58   --packages libgmp3,perl,perl_vendor,rlwrap,unzip,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