diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-05-25 15:03:58 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-05-25 15:03:58 +0200 |
| commit | da49e86de39f8d9ed8709905e63cf442745a904f (patch) | |
| tree | fd8c359b0849c6ff8d8d03b4cd585a5cac10eaaf /engine/univNames.mli | |
| parent | d2533da244f770261478ae829167cb3a8ad38038 (diff) | |
| parent | 9811cda7698652b51e8ebdb25db7285ab8e5ae9a (diff) | |
Merge PR #7556: Add a setting to warn about empty object in the refman
Diffstat (limited to 'engine/univNames.mli')
0 files changed, 0 insertions, 0 deletions