Closed william-r-s closed 8 years ago
Seem to get "Uncaught ReferenceError: corrections is not defined" in developer console in js/main_live.js at 193
@wrsaunde, thanks for the report. I'll check things up.
Fixed.
It was a side-effect of the latest build failure in leanprover/tutorial repo: https://travis-ci.org/leanprover/tutorial/builds/119869686
There was a test failure and js/completion.js
file was not generated correctly as a consequence. I fixed the problem manually for now. I'll update the tutorial soon.
Tutorial claims that you can type \to or \nat and have them replaced by the appropriate symbol, but this functionality doesn't seem to be working (in Chrome on ubuntu)