On 02/07/18 15:20, Max W. Haslbeck wrote:
> Another option would be to set the HGPLAIN environment variable.
> <https://www.mercurial-scm.org/repo/hg/help/environment>
>
>> Am 02.07.2018 um 15:12 schrieb Max W. Haslbeck <max.haslb...@gmx.de
>> <mailto:max.haslb...@gmx.de>>:
>>
>> I found the culprit.
>>
>> In my ~/.hgrc I activated the option:
>> [ui]
>> ...
>> tweakdefaults = True
I did not know of HGPLAIN yet, and have added it here:
changeset: 68566:38c8b44b40b9
user: wenzelm
date: Mon Jul 02 16:26:58 2018 +0200
files: src/Pure/General/mercurial.scala
description:
more robust: avoid dire effect of ui.tweakoptions on hg.known_files;
(I now see that I've got the log message slightly wrong.)
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
