Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[ debug #4647 ] Why on earth is there no highlighting???
These values helped me trace the missing highlighting introduced by the load caused by top-level interaction commands to the agda mode, which supplied "None" as highlighting level to these commands.
- Loading branch information