- printf("PPCIRQMASK: 0x%08X\n", read32(HW_PPCIRQMASK));
-
-
- //??? -- needed?!
- write32(HW_PPCIRQMASK+0x04, 0);
- write32(HW_PPCIRQMASK+0x20, 0);
+ /* ??? -- needed?!
+ * in mini they do
+ *
+ * write32(HW_ARMIRQMASK+0x04, 0);
+ * write32(HW_ARMIRQMASK+0x20, 0);
+ *
+ *
+ * may it's here following; on the other
+ * hand it's already done by mini...
+ *
+ * write32(HW_PPCIRQMASK+0x04+0x08, 0);
+ * write32(HW_PPCIRQMASK+0x20+0x08, 0);
+ */