Benedikt Ahrens

@DanGrayson : your screenshot only shows capitalized file names, hence the order there is alphabetical. What @vladimirias means can be seen, e.g., in CategoryTheory, where we have file names starting...

My opinion is that PRs should compile with the current release and with the development branch of Coq. Maybe this is a discussion rather than an issue? Or do you...

Good with me!

@nmvdw : is this issue solved?

@peterlefanulumsdaine : thanks a lot for the summary. I was not aware of this option until #1672 . The change Peter is suggesting seems beneficial.

I think we can simply try out the change; if it turns out to have consequences we are not anticipating right now, the change can easily be reverted.

To me, these options are not comparable: - Options 1 and 2 seem to be geared towards maintaining the status quo. - Options 3 and 4 seem "dynamic" rather than...

Is the solution here: https://stackoverflow.com/questions/11475221/why-do-i-get-bin-sh-argument-list-too-long-when-passing-quoted-arguments ?

@dwarfmaster : what does the output of `$ readlink -f /bin/sh` show for you? For me it shows `/usr/bin/dash`.

The Coq developers have encountered the same problem with UniMath recently: https://coq.zulipchat.com/#narrow/stream/250632-Coq-Platform-devs-.26-users/topic/Strange.20command.20length.20limit.20on.20Linux