diff options
| author |  Andy Adams-Moran <adams-moran@galois.com> | 2012-05-17 11:00:59 -0700 |
|---|---|---|
| committer | Andy Adams-Moran <adams-moran@galois.com> | 2012-05-17 11:00:59 -0700 |
| commit | 05c1eca7b0257be4babcfa742ba41dc1d7c9058d (patch) | |
| tree | bd34b0261b34a5cd8b6375466a2e2afea39b717b /doc | |
| parent | cde1427223dd0d066b4da59f6834b140ee3322a0 (diff) | |
Doco: ignore generated html
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/manual_src/.gitignore | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/manual_src/.gitignore b/doc/manual_src/.gitignore new file mode 100644 index 0000000..2d19fc7 --- /dev/null +++ b/doc/manual_src/.gitignore @@ -0,0 +1 @@ +*.html |