Flush command added

diff --git a/Robust/src/ClassLibrary/FileOutputStream.java b/Robust/src/ClassLibrary/FileOutputStream.java
index ed81ed7cd35ae2be458ddf95f1900cd1bf55d642..031634ff1930e1217222795a30505880b601f7f6 100644 (file)
--- a/Robust/src/ClassLibrary/FileOutputStream.java
+++ b/Robust/src/ClassLibrary/FileOutputStream.java
@@ -21,6 +21,7 @@ public class FileOutputStream {
     private static native int nativeAppend(byte[] filename);
     private static native void nativeWrite(int fd, byte[] array);
     private static native void nativeClose(int fd);
+    private static native void nativeFlush(int fd);
     
     public void write(int ch) {
        byte b[]=new byte[1];
@@ -32,6 +33,10 @@ public class FileOutputStream {
        nativeWrite(fd, b);
     }
 
+    public void flush() {
+       nativeFlush(fd);
+    }
+
     public void close() {
        nativeClose(fd);
     }

diff --git a/Robust/src/Runtime/file.c b/Robust/src/Runtime/file.c
index fa8343dcbdf05d519c99127ccd1533ed960ff3c3..88cd585c95c8cca8bddd825ee75c72e1eb98b0e8 100644 (file)
--- a/Robust/src/Runtime/file.c
+++ b/Robust/src/Runtime/file.c
@@ -17,6 +17,10 @@ void ___FileOutputStream______nativeClose____I(int fd) {
   close(fd);
 }
 
+void ___FileOutputStream______nativeFlush____I(int fd) {
+  fsync(fd);
+}
+
 int ___FileOutputStream______nativeOpen_____AR_B(struct ArrayObject * ao) {
   int length=ao->___length___;
   char* filename= (((char *)& ao->___length___)+sizeof(int));