diff options
author | Michael Schmidt <github@mschmidt.me> | 2017-01-17 10:23:40 +0100 |
---|---|---|
committer | Michael Schmidt <github@mschmidt.me> | 2017-01-17 10:23:40 +0100 |
commit | 629b90d8d88128bab1cb4ad5e533d8f3c82730f3 (patch) | |
tree | f8e2fd06b91d131515abe287dc93f07d9d9e84f1 /doc/ccomp.1 | |
parent | 43db836ea4fb19036a19f78e1f988f75a42b910c (diff) | |
download | compcert-629b90d8d88128bab1cb4ad5e533d8f3c82730f3.tar.gz compcert-629b90d8d88128bab1cb4ad5e533d8f3c82730f3.zip |
bug 20679, more precise description of -g
Diffstat (limited to 'doc/ccomp.1')
-rw-r--r-- | doc/ccomp.1 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/ccomp.1 b/doc/ccomp.1 index ef4d7743..c02d3571 100644 --- a/doc/ccomp.1 +++ b/doc/ccomp.1 @@ -219,7 +219,7 @@ Debugging Options . .TP .B \-g -Generate debugging information. +Generate full debugging information. . .TP .BR \-g0 ", " \-g1 ", " \-g2 ", " \-g3 |