diff options
| author | Gaëtan Gilbert | 2018-02-21 11:52:31 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-02-21 11:52:31 +0100 |
| commit | 6938d81c37467073d0bd731c0ef9e3feed92fb2f (patch) | |
| tree | 1afddd5dbe1fdf90b87d937f10954d273e879419 /pretyping/typeclasses_errors.ml | |
| parent | aec63ba9c8f6840d98ba731640a786138d836343 (diff) | |
coqdev.el: add space at the end of compile-command
That way you can just type [-j] instead of having to remember to add a
space yourself.
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
0 files changed, 0 insertions, 0 deletions