From bf57a5d79caa8e49cd41f776708ed2865f411996 Mon Sep 17 00:00:00 2001 From: Alexander Boettcher Date: Thu, 9 Jan 2014 09:22:08 +0100 Subject: [PATCH] pci: increase memory for device pd not enough anymore on 32 bit after #989 changes --- os/src/drivers/pci/main.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/os/src/drivers/pci/main.cc b/os/src/drivers/pci/main.cc index 86927fe588..27e4bb3228 100644 --- a/os/src/drivers/pci/main.cc +++ b/os/src/drivers/pci/main.cc @@ -81,7 +81,7 @@ int main(int argc, char **argv) */ enum { STACK_SIZE = 2 * sizeof(addr_t)*1024, - PCI_DEVICE_PD_RAM_QUOTA = sizeof(addr_t) * 128 * 1024, + PCI_DEVICE_PD_RAM_QUOTA = 196 * 4096, }; static Cap_connection cap;