--- src/devices/bus_pci.c.orig	2008-01-18 21:12:27.000000000 +0200
+++ src/devices/bus_pci.c	2008-02-02 12:49:54.000000000 +0200
@@ -784,6 +784,8 @@
 			wdc_set_io_enabled(wdc0, enabled);
 		if (wdc1 != NULL)
 			wdc_set_io_enabled(wdc1, enabled);
+		/*  Set all bits:  */
+		PCI_SET_DATA(reg, value);
 		return 1;
 	}