Tan Yee Jian

Results 7 comments of Tan Yee Jian

I have the same issue too, using NeoVim 0.5-dev. The variable is simply unchanged.

Having the same problem while installing via OPAM. However, I found that `z3>=4.8.13` (latest is [4.11.2](https://opam.ocaml.org/packages/z3/z3.4.11.2/)) would no longer need the deprecated Python 2.7 and uses Python 3 instead. I...

Related: https://github.com/FStarLang/FStar/issues/2431

I got the following error, some personal info truncated. ``` 15:03:28.933 [error] %CaseClauseError{term: {:error, {:unexpected_content, %HTTPoison.Response{body: "{\"code\":400,\"status\":\"fail\",\"message\":\"Input is not valid.\"}", headers: [{"Cache-Control", "no-store,no-cache"}, {"Pragma", "no-cache"}, {"Transfer-Encoding", "chunked"}, {"Content-Type", "application/json; charset=utf-8"},...

> Documentation is missing. I have just added some minimal documentation (for the [flag](https://agda--7861.org.readthedocs.build/en/7861/tools/command-line-options.html#cmdoption-cubical-without-glue) and on the [Cubical](https://agda--7861.org.readthedocs.build/en/7861/language/cubical.html) page), let me know if you think we need more. > Is...

> I think the documentation should include something about how the options interact (which is [somewhat complicated](https://agda.readthedocs.io/en/v2.7.0.1/language/cubical.html#cubical-agda-with-erased-glue) in the case of `--erased-cubical` and `--cubical`). https://github.com/agda/agda/pull/7861/commits/59e6946b61c80fed516ef55bc9213b07c6852594 adds more detailed documentation [as...

This is now ready for another round of review. The technical changes stay the same, while the `--cubical-without-glue` flag is renamed into `--cubical=no-glue`, along with the aliasing of the other...