[isabelle-dev] Isabelle build only works in certain directories
makarius at sketis.net
Mon Jul 2 16:42:36 CEST 2018
On 02/07/18 15:20, Max W. Haslbeck wrote:
> Another option would be to set the HGPLAIN environment variable.
>> Am 02.07.2018 um 15:12 schrieb Max W. Haslbeck <max.haslbeck at gmx.de
>> <mailto:max.haslbeck at gmx.de>>:
>> I found the culprit.
>> In my ~/.hgrc I activated the option:
>> tweakdefaults = True
I did not know of HGPLAIN yet, and have added it here:
date: Mon Jul 02 16:26:58 2018 +0200
more robust: avoid dire effect of ui.tweakoptions on hg.known_files;
(I now see that I've got the log message slightly wrong.)
More information about the isabelle-dev