diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-22 11:06:04 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-07-07 16:34:43 +0200 |
| commit | 4b3187a635864f8faa2d512775231a4e6d204c51 (patch) | |
| tree | 6ed32cd7b3f8530336c43137f0603200dc69098b /dev | |
| parent | fe371675fc85d712f5124d73157bd833e8fa14a6 (diff) | |
Remove dead code that used to be there for CamlpX compatibility.
Part of this code has been introduced very recently in 7c62654 in spite of
the existence of a proper API. This means that this should be better
documented.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions