Robert Estelle

@scottchiefbaker — Thanks for the input and additional measurements. The timing isn't close to what I'd measured, so I think something else must be going on. Note that the benchmark...

> Do you know what version of Git git config --get-color was added in? Is this a newer Git thing, or has it been around forever? Forever—some digging shows it...

This doesn't need to be an all-or-nothing thing; for warnings that defy brief description, numeric codes can always be used first. (Or, human codes could cover multiple numeric codes; some...

@syrusakbary This PR looks good, is anything preventing it from merging?

@syrusakbary I think you're mostly right, but a couple considerations: 1. There are some better-performing serialization libraries that, if installed, are nice to use: http://artem.krylysov.com/blog/2015/09/29/benchmark-python-json-libraries/ 2. One of the use-cases...

@favonia If it helps provide context, that change was introduced here: https://github.com/agda/agda/pull/3419 and @jespercockx [began some partial fixes](https://github.com/agda/agda/pull/3419#issuecomment-443139996) here: https://github.com/jespercockx/HoTT-Agda/commit/a15f184df73304a7bfeeaac96194b89286501bdb However, those fixes are incomplete. Like he commented, I'm also...

@jek I understand your determinism objection and definitely agree. Will fix. I'm also removing the global namespace exposure here, though I think I disagree and would like to look at...

@jek This has been rebased and squashed with your suggestions. The global namespace exposure has been moved into #24

I wrestled with this today too. All I wanted was to get `apply-refact` to actually delete unused language pragmas instead of leaving blank lines…but the annotation offsets are inscrutable and...

Yes, but that was already a hazard of having those two branch names to begin with under `refs/heads`.