diff options
| author | Théo Zimmermann | 2019-05-07 19:35:17 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-23 21:39:55 +0200 |
| commit | c7cc87ef2d05706a0a40f7a2d296055cf48fc7c0 (patch) | |
| tree | 9464d9c43e0208d77c1b94e0141cb1f814730849 /plugins/derive/plugin_base.dune | |
| parent | 5cfdc20560392c2125dbcee31cfd308d5346b428 (diff) | |
Make progress toward #9411: reject new undefined references.
We list preexisting undefined tokens explicitly in
`doc/sphinx/conf.py` and prevent new ones from being introduced by
making it a fatal warning.
This list should be seen as a TODO. Once it is emptied, #9411 can be
closed.
Diffstat (limited to 'plugins/derive/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions