XXX nobios

*** 34,44 ****
   * Numerous platform-dependent interfaces that don't seem to belong
   * in any other header file.
   *
   * This file should not be included by code that purports to be
   * platform-independent.
-  *
   */
  
  #include <sys/machparam.h>
  #include <sys/varargs.h>
  #include <sys/thread.h>
--- 34,43 ----
*** 230,239 ****
--- 229,240 ----
  extern page_t *page_get_high_mfn(mfn_t);
  #endif
  
  extern hrtime_t tsc_gethrtime_tick_delta(void);
  
+ extern boolean_t bios_calls_available;
+ 
  #endif /* _KERNEL */
  
  #ifdef __cplusplus
  }
  #endif