used by if_timer is reserved for expanding if_index to an int in the future. Reviewed by: rwatson, brooks
pointers to "dead" implementations that no-op rather than invoking the device driver. This would generally be unexpected and possibly quite badly handled by most device drivers after if_detach() has completed. Reviewed by: bms MFC after: 3 weeks