diff options
| author | Ramana Kumar | 2018-05-21 10:21:20 +0100 |
|---|---|---|
| committer | Ramana Kumar | 2018-05-21 10:21:20 +0100 |
| commit | 66781e49fb339071d9915b3bc42fca7f250a567b (patch) | |
| tree | 22431fd11614fe24a94894ea17c62a2b95e9b659 /language/primitive_doc.ott | |
| parent | e2aa34b0ba28d89eab9f845fe904d4fdebb17395 (diff) | |
Ignore src/share_directory.ml
src/Makefile suggests this is a generated file
Diffstat (limited to 'language/primitive_doc.ott')
0 files changed, 0 insertions, 0 deletions