search

leanprover / leanprover.github.io

www
https://lean-lang.org/
15 stars 24 forks source link

unicode shortcuts are not working anymore #49

Closed leodemoura closed 8 years ago

leodemoura commented 8 years ago

In the past, we could use shortcuts such as \to, \nat and \fun in the Lean web version. It doesn't seem to work anymore. I tried in different browsers on Windows and Linux. It doesn't work in any of them.

@soonhokong Do you have any idea why it doesn't work anymore?

@avigad Does it work for you?

Thanks.

soonhokong commented 8 years ago

It's because js/input-method.js is not properly generated (now it's empty). I'll fix it soon.

leodemoura commented 8 years ago

Thanks.

soonhokong commented 8 years ago

I manually update js/input-method.js. It should work now.

We automatically generate this file from travis-ci, something changes and now it breaks. I'll investigate it and fix the problem soon.

leodemoura commented 8 years ago

BTW, Bryan @parno was the one that found the problem.

leodemoura commented 8 years ago

I manually update js/input-method.js. It should work now.

I cleared the cache, and tried again. It still doesn't work. Does it take a few minutes for the change to propagate?

soonhokong commented 8 years ago

@leodemoura, there was a problem. Now it should work. I checked that it worked on my machines.

avigad commented 8 years ago

It is working for me too.

leodemoura commented 8 years ago

@soonhokong It is working for me now. Thanks for fixing it!

@parno The problem was fixed.

parno commented 8 years ago

Yep, working for me as well. Thanks for the fix!

soonhokong commented 8 years ago

FYI, this fix was a temporary one. There is still a problem in Travis-CI and I'm working with them to fix it (mainly to upgrade its emacs-24 installation from the currently deprecated one). When it's done, I'll let you know with another comment. Until then, I'll do manual updates of js/input-method.el file whenever we have a new commit on the leanprover/tutorial repo.