text: /*
   * Copyright 2014, NICTA
   *
   * This software may be distributed and modified according to the terms of
   * the BSD 2-Clause license. Note that NO WARRANTY is provided.
   * See "LICENSE_BSD2.txt" for details.
   *
   * @TAG(NICTA_BSD)
   */
  
  #include <sel4/sel4.h>
  
  /** Consider moving bootinfo into libsel4_startup */
  seL4_BootInfo* bootinfo;
  
  /** Consider moving seL4_InitBootInfo into libsel4_startup */
  void seL4_InitBootInfo(seL4_BootInfo* bi)
  {
      bootinfo = bi;
      /* Save the address of the IPC buffer for seL4_GetIPCBuffer on IA32. */
      seL4_SetUserData((seL4_Word)bootinfo->ipcBuffer);
  }
  
  seL4_BootInfo* seL4_GetBootInfo()
  {
      return bootinfo;
  }
  