merged;
authorwenzelm
Fri, 24 Oct 2014 20:49:23 +0200
changeset 58781 c385da5c665e
parent 58778 e29cae8eab1f (current diff)
parent 58780 1f8c0da85664 (diff)
child 58782 7305bad408b5
merged;
--- a/Admin/PLATFORMS	Thu Oct 23 19:40:41 2014 +0200
+++ b/Admin/PLATFORMS	Fri Oct 24 20:49:23 2014 +0200
@@ -93,10 +93,8 @@
   shell /bin/sh is *not* appropriate, because there are too many
   non-standard implementations of it.
 
-* Perl as largely portable system programming language.  In some
-  situations Python may serve as an alternative, but it usually
-  performs not as well in addressing various delicate details of
-  operating system concepts (processes, signals, sockets etc.).
+* Perl as largely portable system programming language, with its
+  fairly robust support for processes, signals, sockets etc.
 
 * Scala with Java 1.7.  Isabelle/Scala irons out many oddities and
   portability issues of the Java platform.
--- a/Admin/components/components.sha1	Thu Oct 23 19:40:41 2014 +0200
+++ b/Admin/components/components.sha1	Fri Oct 24 20:49:23 2014 +0200
@@ -11,6 +11,7 @@
 3dc680d9eb85276e8c3e9f6057dad0efe2d5aa41  cygwin-20140626.tar.gz
 8e562dfe57a2f894f9461f4addedb88afa108152  cygwin-20140725.tar.gz
 238d8e30e8e22495b7ea3f5ec36e852e97fe8bbf  cygwin-20140813.tar.gz
+629b8fbe35952d1551cd2a7ff08db697f6dff870  cygwin-20141024.tar.gz
 0fe549949a025d65d52d6deca30554de8fca3b6e  e-1.5.tar.gz
 2e293256a134eb8e5b1a283361b15eb812fbfbf1  e-1.6-1.tar.gz
 e1919e72416cbd7ac8de5455caba8901acc7b44d  e-1.6-2.tar.gz
--- a/Admin/lib/Tools/makedist_cygwin	Thu Oct 23 19:40:41 2014 +0200
+++ b/Admin/lib/Tools/makedist_cygwin	Fri Oct 24 20:49:23 2014 +0200
@@ -55,7 +55,7 @@
   --site "$CYGWIN_MIRROR" --no-verify \
   --local-package-dir 'C:\temp' \
   --root "$(cygpath -w "$TARGET")" \
-  --packages libgmp3,perl,perl_vendor,python,rlwrap,unzip,vim \
+  --packages libgmp3,perl,perl_vendor,rlwrap,unzip,vim \
   --no-shortcuts --no-startmenu --no-desktop --quiet-mode
 
 [ "$?" = 0 -a -e "$TARGET/etc" ] || exit 2
--- a/src/Tools/jEdit/src/jEdit.props	Thu Oct 23 19:40:41 2014 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Fri Oct 24 20:49:23 2014 +0200
@@ -8,6 +8,7 @@
 buffer.noTabs=true
 buffer.sidekick.keystroke-parse=false
 buffer.tabSize=2
+buffer.undoCount=1000
 close-docking-area.shortcut2=C+e C+CIRCUMFLEX
 complete-word.shortcut=
 console.dock-position=floating