George Agapov

For now it seems to be a low priority

!ci-toolchain-me

!ci-build-me

!ci-toolchain-me

!ci-build-me

!ci-build-me

!ci-build-me

So the issue is the following: ``` git checkout origin/berkeley ./nix/pin.sh # just pins the submodules git checkout origin/develop ./nix/pin.sh git status ``` will give following output for the last...

I suggest the following two remedies to avoid unnecessary friction: 1. Add `src/external` to `.gitignore` 2. Add `(data_only_dirs external)` to `src/dune` This way we'll ensure neither git nor dune will...

Is this change necessary in `berkeley`? It looks safe and sane, but I'd prefer to avoid **any** changes to `berkeley` unless we're confident they're necessary. As for these changes, I...