diff options
| -rw-r--r-- | kernel/entries.mli (renamed from intf/entries.mli) | 0 |
1 files changed, 0 insertions, 0 deletions
diff --git a/intf/entries.mli b/kernel/entries.mli index 2460ec6445..2460ec6445 100644 --- a/intf/entries.mli +++ b/kernel/entries.mli |