equal
deleted
inserted
replaced
61 [ "$?" = 0 -a -e "$TARGET/etc" ] || exit 2 |
61 [ "$?" = 0 -a -e "$TARGET/etc" ] || exit 2 |
62 |
62 |
63 |
63 |
64 # patches |
64 # patches |
65 |
65 |
66 for NAME in hosts protocols services networks |
66 for NAME in hosts protocols services networks passwd group |
67 do |
67 do |
68 rm "$TARGET/etc/$NAME" |
68 rm "$TARGET/etc/$NAME" |
69 done |
69 done |
70 |
70 |
71 ln -s cygperl5_14.dll "$TARGET/bin/cygperl5_14_2.dll" |
71 ln -s cygperl5_14.dll "$TARGET/bin/cygperl5_14_2.dll" |
72 |
72 |
73 rm "$TARGET/Cygwin.bat" |
73 rm "$TARGET/Cygwin.bat" |
74 |
74 |
75 cp -a "$ISABELLE_HOME/Admin/Windows/Cygwin/isabelle/." "$TARGET/isabelle/." |
75 for NAME in init.bat postinstall rebaseall |
|
76 do |
|
77 cp -a "$ISABELLE_HOME/Admin/Windows/Cygwin/isabelle/$NAME" "$TARGET/isabelle/." |
|
78 done |
76 |
79 |
77 |
80 |
78 # archive |
81 # archive |
79 |
82 |
80 DATE=$(date +%Y%m%d) |
83 DATE=$(date +%Y%m%d) |