Use better optimisation options.

diff --git a/plat/linux386/pmfile b/plat/linux386/pmfile
index 24adc42..87e20ba 100644 (file)
--- a/plat/linux386/pmfile
+++ b/plat/linux386/pmfile
@@ -25,7 +25,7 @@ local headers = group {
 platform_linux386 = group {
        ARCH = "i386",
        PLATFORM = "linux386",
-       OPTIMISATION = "-O",
+       OPTIMISATION = "-O6",
        
        -- Ensure the descr and headers are installed first because we'll need it
        -- to build the libraries.

diff --git a/plat/pc86/pmfile b/plat/pc86/pmfile
index 0afe6a5..f7d5733 100644 (file)
--- a/plat/pc86/pmfile
+++ b/plat/pc86/pmfile
@@ -25,7 +25,7 @@ local headers = group {
 platform_pc86 = group {
        ARCH = "i86",
        PLATFORM = "pc86",
-       OPTIMISATION = "-O",
+       OPTIMISATION = "-O6",
        
        -- Ensure the descr and headers are installed first because we'll need
        -- them to build the libraries.