brifuture:

As the problem disappeared, shall I create an issue on GitHub?


I don’t think it would be helpful, if you (and thus we) cannot reproduce it.
In case you are running into this issue again and can reproduce it, please create an issue.