Re: [isabelle-dev] jedit: zoom with cmd++

2012-12-22 Thread Makarius
On Wed, 19 Dec 2012, Steffen Juilf Smolka wrote: in a39250169636, it is possible to increase/decrease the font size in jedit with cmd++/cmd+- on MacOS (probably ctrl++/ctrl+- on other plattforms) (nice feature!). However, pressing cmd++ increases the font size twice on my machine (cmd+- works

Re: [isabelle-dev] Repository Trouble

2012-12-22 Thread Makarius
On Fri, 21 Dec 2012, Jasmin Christian Blanchette wrote: Am 20.12.2012 um 21:30 schrieb Alexander Krauss: On 12/20/2012 12:20 AM, Alexander Krauss wrote: (2) The local sysadmins are working on replacement of the Mercurial 2.4 from SuSE 12.2, which is potentially the cause problems here.