XXX nobios

@@ -34,11 +34,10 @@
  * 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>

@@ -230,10 +229,12 @@
 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