I don't know anything about a bug in unify/reformat. Sometimes bad unify commands will throw up a console error and manifest in the UI as a unify that doesn't stop and has to be cancelled. If so, please show the error. Otherwise, I don't know what this could be, and I would be interested to hear if it is also triggered in the master version.
Mario On Wed, Mar 18, 2020 at 8:23 AM Benoit <[email protected]> wrote: > Thanks, I'm going to try to download master and/or downgrade JDK. > > Note that my problem is with Ctrl-U, which is "unify", not "undo", and > with Ctrl-R (reformat). > > > Benoît > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/17e931b9-e063-4167-abee-dfba744e8f04%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/17e931b9-e063-4167-abee-dfba744e8f04%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSvvu8_Kz%2B43Fe82TKckf1x6hd9gO0t_2Lmvvkfs2CE9XQ%40mail.gmail.com.
