# HG changeset patch
# User Paul Boddie <paul@boddie.org.uk>
# Date 1680810499 -7200
# Node ID 06eb2b9ef9e7e23fa2b7ec866db098bd6a74ba85
# Parent  d3c01405b62d524336f4ec7ad89a37ab97ca803a
Attempted to fix detach operation behaviour due to the inscrutable L4Re API.

diff -r d3c01405b62d -r 06eb2b9ef9e7 libsystypes/idl/region_mapper.idl
--- a/libsystypes/idl/region_mapper.idl	Thu Apr 06 21:47:16 2023 +0200
+++ b/libsystypes/idl/region_mapper.idl	Thu Apr 06 21:48:19 2023 +0200
@@ -15,11 +15,17 @@
                           in address_t offset, in unsigned char align);
 
   /* Detach memory from the task, searching from the given address for a region
-     of the given size. Return the start address, region size and dataspace. */
+     of the given size. Return the start address, region size and dataspace.
+     Note that the dataspace is returned as an index, not an actual capability.
+
+     See: pkg/l4re-core/l4re/include/rm
+     See: pkg/l4re-core/l4sys/include/cxx/ipc_iface
+
+     This is not obvious from the L4Re definitions and the IPC type system. */
 
   [opcode(1)] void detach(in address_t addr, in address_t size,
                           in map_flags_t flags, out address_t start,
-                          out address_t rsize, out cap ds);
+                          out address_t rsize, out l4_cap_idx_t ds);
 
   /* Find a region starting from the given address and having the given size.
      Return the start address, region size and dataspace. */