Ali Caglayan
Ali Caglayan
We had some compat code leftover.
[Here is a branch of mine](https://github.com/Alizter/HoTT/tree/spec2) that has the colimits and EM spaces branches merged. I have changed the definition of `Build_Spectrum` so that it will demand all the data....
I was setting up a isolate_post_checkout but I didn't mark it is executable. The warning was helpful but it looks like the path has a double `//`. ``` /home/ali/dune//.git/git-ps/hooks/isolate_post_checkout but...
According to the [structopt repo](https://github.com/TeXitoi/structopt) the project is in maintenance mode and has been integrated into [clap](https://github.com/clap-rs/clap). We should perhaps think of migrating to that. clap has a number of...
As discussed on slack, it might be nice to have `gps` autostash the dirty git tree when doing `git rr`. On the other hand, people should really be making WIP...
We should document the workflow where you have rr'd a patch and then a collaborator pushes their own commits in your PR and you want to squash them into your...
With Notty it is possible to check for mouse events and modifier keys together. For example shift scrolling. This doesn't appear to be possible in nottui.
Contrary to Notty.I.zcat the order of composition for Ui.zcat appears to be reversed.
Code completion gives suggestions about what the user might want to type. We need to investigate groups of objects and priorities.
The _CoqProject finding logic doesn't handle the case when _CoqProject appears in a subdirectory of a workspace. This can happen if a certain folder contains all the Coq related things....