diff options
author | 2017-04-24 14:12:13 +0200 | |
---|---|---|
committer | 2017-04-24 14:12:13 +0200 | |
commit | 3e50f0a7e356b2fcb1cf22ec95549a7322e4e447 (patch) | |
tree | 62e05d0d245fd305a8e821ffd8a694d3786e686b /kernel/pre_env.mli | |
parent | 3ba5dc3be9767422a6874fef034041a36b34f620 (diff) | |
parent | 59bb9b37c58e8b5f8d009d598e949aa995e6973e (diff) |
Merge PR#581: [toplevel] [emacs] Don't quote errors in emacs mode.
Diffstat (limited to 'kernel/pre_env.mli')
0 files changed, 0 insertions, 0 deletions