diff options
| author | Gabriel Kerneis | 2014-04-23 14:35:02 +0100 |
|---|---|---|
| committer | Gabriel Kerneis | 2014-04-23 15:00:56 +0100 |
| commit | cd0728219401bf4b7dd8d43db7927d436318fd70 (patch) | |
| tree | a90bdb9d814b1bbbb320261f16779b5ad528a49a /.gitignore | |
| parent | d9f3b585c5ccbffba88cb404287e95ec77bbaa76 (diff) | |
make doc
Build html doc of module interface
Diffstat (limited to '.gitignore')
| -rw-r--r-- | .gitignore | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -1,6 +1,7 @@ *.native *.byte src/_build/ +src/sail.docdir language/*.pdf language/*.uo language/*.ui |