diff options
author | Michael Schmidt <github@mschmidt.me> | 2017-02-15 13:46:39 +0100 |
---|---|---|
committer | Michael Schmidt <github@mschmidt.me> | 2017-02-15 13:46:39 +0100 |
commit | 70ec998cfda48dcef37368cf2712736949e378fc (patch) | |
tree | d311376913446c03121ecf6e21ea1a3ad3517ef3 /doc/ccomp.1 | |
parent | 1aee802bf438fff7a83dec4607cabefdc398c3de (diff) | |
download | compcert-70ec998cfda48dcef37368cf2712736949e378fc.tar.gz compcert-70ec998cfda48dcef37368cf2712736949e378fc.zip |
drop .cm support from man page
Diffstat (limited to 'doc/ccomp.1')
-rw-r--r-- | doc/ccomp.1 | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/doc/ccomp.1 b/doc/ccomp.1 index d84adc7f..31282cb3 100644 --- a/doc/ccomp.1 +++ b/doc/ccomp.1 @@ -27,10 +27,6 @@ C source file. C source file that should not be preprocessed. . .TP -.B .cm -Cminor source file. -. -.TP .B .s Assembly file. . |