Nils Anders Danielsson

The error message should be better.

For the Emacs implementation: One can attach information ("text properties") to text in the buffer. We already do this for the go-to functionality (use `C-u C-x =` to see the...

Perhaps the problem can be fixed by moving the `touch src/full/Agda/VersionCommit.hs` hack to `Setup.hs`. In that case care should be taken to ensure that the hack works on all supported...

The `touch` hack does not seem to work very well when GHC 9.4.2 is used. My guess is that GHC is now better at avoiding recompilation. An alternative is perhaps...

A [discussion](https://github.com/s5k6/versionInfo) about this kind of thing.

Is this a regression? In that case you could use bisection.

> which you did not describe, so I added the description > > > (Andreas: Goal of this PR: speed up generation of .agdai files during setup.) There was a...

> "Fixed #nnn" isn't a sufficient description. An issue #nnn only describes the _problem_. A PR should describe the _solution_. In particular _what_ solution has been taken, and sometimes also...

Are there other potential pitfalls related to file names?

I think we should aim for maximum portability: * Only printable 7-bit ASCII characters. * Not `/`, `\`, or `.`, and no lower-case letters. In fact, for simplicity, let's only...