diff options
| author | Emilio Jesus Gallego Arias | 2018-09-27 02:25:16 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-01 05:00:01 +0200 |
| commit | ec1e83e85543a793dc248e9d2f47dd146f9a913d (patch) | |
| tree | 185f31099afb50d4ebcdaf5d292aff78c0ae00ef /kernel | |
| parent | c155259dee7e4b2bfafe42375b45f2f4d6c6cfbd (diff) | |
[envars] Defer CAMLP5 location to configure.
These functions are unused, and configure should suffice for this
purpose.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions