jhb 4dd39ab878 Rename the IPI API from smp_ipi_* to ipi_* since the smp_ prefix is just
"redundant noise" and to match the IPI constant namespace (IPI_*).

Requested by:	bde
2001-04-11 17:06:02 +00:00
..
2000-10-24 10:49:56 +00:00
2001-03-24 15:17:27 +00:00
2000-10-24 10:49:56 +00:00