I've been playing around recently with the `github-merge.py` script recently; and while I've been able to create merges with it (see 73c90c8370 and 10ddf62dfb)
it complains / refuses to trivially work with symlinks. I haven't been able to figure out exactly why it doesn't want symlinks, but I think it's related to the sha512sum hash that gets created.
I'm not sure if we'll start using `github-merge.py` more or not; but I guess we should "fix" this anyhow in order to learn more how these work. It may be useful to move to merging commits locally and not relying on github being a good actor? 🤷
* build: detect the presence of libgmp before generating Makefile
* depends: add arximboldi/immer@v0.6.2 as a package and add detection
* depends: remove immer from source tree, build using package only
* Drop immer refs from tools
Co-authored-by: UdjinM6 <UdjinM6@users.noreply.github.com>
* Update immer library to current master (0a718d2d76bab6ebdcf43de943bd6c7d2dbfe2f9)
* Temporary fix for alignof(std::max_align_t) on MinGW 32bit builds
See https://github.com/arximboldi/immer/issues/78
