diff options
| author | Luc Van Oostenryck <luc.vanoostenryck@gmail.com> | 2018-02-24 11:40:45 +0100 |
|---|---|---|
| committer | Luc Van Oostenryck <luc.vanoostenryck@gmail.com> | 2018-05-21 02:49:43 +0200 |
| commit | d22015775e0b76ccf64ad1f8afc68443c308fbce (patch) | |
| tree | 219d7b150bcd4b622d7c2afc8b3cf46e39ee74cc /Documentation/.gitignore | |
| parent | b048f49bd28074bcbdc7506f1a61b48c842633ed (diff) | |
| download | sparse-dev-d22015775e0b76ccf64ad1f8afc68443c308fbce.tar.gz | |
doc: format dev-options.md as a man page
The file dev-options.md contains the description for extra
options not useful for sparse itself and its users but well
to sparse's developers and for tools like test-linearize.
Since it's a complement to the main man-page, format it at such.
Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
Diffstat (limited to 'Documentation/.gitignore')
| -rw-r--r-- | Documentation/.gitignore | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Documentation/.gitignore b/Documentation/.gitignore index 378eac25..6c08d03c 100644 --- a/Documentation/.gitignore +++ b/Documentation/.gitignore @@ -1 +1,2 @@ build +dev-options.1 |