Thomas Leonard

It blocks for the whole time the server is running, not just until it starts.

For others with this problem, this seems to work: 1. Do everything up to and including the `dune-release distrib` step as usual. 2. Edit your main opam file to set...

I tried deleting the token file and letting dune-release recreate it with 1.4.0, and it didn't help. It failed with both the old and new GitHub token formats. But using...

> As you question, do we want the user to have the possibility to escape from the build directory and make the user responsible for that or not? Who is...

We now support the GitHub checks API, which provides something similar (but it appears in the Checks tab instead of in a comment).

Yeah, improving this could certainly be useful. It wasn't in its own package because it didn't add any dependencies. If it's adding irmin-watcher then it does need to be moved...

Note: the [Git comment]( https://github.com/ocurrent/ocurrent/commit/7ed02003b142ea5e632eb58eefdef5b3fe2b3b1f) for the previous code says: > copy local Git directories instead of cloning so that the pack files and timestamps don't change and mess up...

Do you need the `.git` directory in the clone? If not, you could probably just `git checkout --work-tree=/repo/dir /tmp/dir`. There should probably be a separate `with_export` or something to do...

Not `git worktree` (that's something else). `git --work-tree` should apply to all commands - it's documented in `man git`. e.g. ``` mkdir /tmp/a git --work-tree=/tmp/a checkout HEAD /tmp/a ls /tmp/a...

I think there should be two functions: one to clone with .git and one without (or it could be an argument to say which you want). If you only have...