1.1 --- a/Admin/build	Thu Sep 12 13:48:17 2013 +0200
     1.2 +++ b/Admin/build	Thu Sep 12 14:06:08 2013 +0200
     1.3 @@ -74,7 +74,7 @@
     1.4  
     1.5  ## main
     1.6  
     1.7 -#workaround for scalac
     1.8 +#workaround for scalac 2.10.2
     1.9  function stty() { :; }
    1.10  export -f stty
    1.11  

     2.1 --- a/src/Tools/Graphview/lib/Tools/graphview	Thu Sep 12 13:48:17 2013 +0200
     2.2 +++ b/src/Tools/Graphview/lib/Tools/graphview	Thu Sep 12 14:06:08 2013 +0200
     2.3 @@ -139,7 +139,7 @@
     2.4    rm -rf classes && mkdir classes
     2.5  
     2.6    (
     2.7 -    #workaround for scalac
     2.8 +    #workaround for scalac 2.10.2
     2.9      function stty() { :; }
    2.10      export -f stty
    2.11  

     3.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Thu Sep 12 13:48:17 2013 +0200
     3.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Thu Sep 12 14:06:08 2013 +0200
     3.3 @@ -287,7 +287,7 @@
     3.4  
     3.5    cp -p -R -f "${JEDIT_JARS[@]}" dist/jars/. || failed
     3.6    (
     3.7 -    #workaround for scalac
     3.8 +    #workaround for scalac 2.10.2
     3.9      function stty() { :; }
    3.10      export -f stty
    3.11