Kevin Sullivan

Ok this is good. The lean download and installation page should probably be updated at least to notify people of this fact. Thanks! On Tue, Sep 4, 2018, 2:20 PM...

Thanks for this work-around. --Kevin

> > > @stewart1969 You can get burned in captions via text sources. > Just add a text source to your scene(s) in OBS and then in the caption settings...

> > > > @stewart1969 You can get burned in captions via text sources. > > Just add a text source to your scene(s) in OBS and then in the...

Thanks. My students have docker desktop installed because I require it. Otherwise usually not. But this packaging had worked well for me for several years and classes of 100 first...

I deliver the Lean Prover to them this way, in discrete math class for second semester undergrads. On Wed, Oct 5, 2022, 6:50 PM Kevin Sullivan ***@***.***> wrote: > Thanks....

> > > @kevinsullivan it seems that Docker Desktop UI lost the connection with the Dev Environments backend, can you restart Docker Desktop and retry? > If you still have...

> > > @kevinsullivan it seems that Docker Desktop UI lost the connection with the Dev Environments backend, can you restart Docker Desktop and retry? > If you still have...

Some more information. I suspect that the error being reported might be an unhandled exception due to my failing attempt in the Docker file to copy a .profile file from...

Okay, apparently not all alphanumeric characters are supported as subscripts in the unicode definitions being used here: http://ftp.unicode.org/Public/UNIDATA/UnicodeData.txt. I suggest adding the following sentence to the end of the first...