commit d49cb12f62f7a9f2f9835787b292f9885ab99bc2
author Thomas Heijligen <src@posteo.de> Wed Nov 29 10:03:02 2023 +0000
committer Thomas Heijligen <src@posteo.de> Wed Nov 29 10:03:02 2023 +0000
tree 91293e5aaf2bde9f64adaf5bab8ef8f94d58955c
parent b00b3166219e072b759b2d9855ef5e12d0a75552

Move SPARK_Mode => Off into body

Signed-off-by: Thomas Heijligen <src@posteo.de>

src/fs-filo-vfs.adb

diff --git a/src/fs-filo-vfs.adb b/src/fs-filo-vfs.adb
index 75df52b..30f1bca 100644
--- a/src/fs-filo-vfs.adb
+++ b/src/fs-filo-vfs.adb
@@ -3,7 +3,11 @@
 
 use Interfaces.C;
 
-package body FS.FILO.VFS is
+package body FS.FILO.VFS
+with
+   SPARK_Mode => Off,
+   Convention => C
+is
 
    function C_Mount return int
    is

src/fs-filo-vfs.ads

diff --git a/src/fs-filo-vfs.ads b/src/fs-filo-vfs.ads
index 95fa71d..6115554 100644
--- a/src/fs-filo-vfs.ads
+++ b/src/fs-filo-vfs.ads
@@ -13,11 +13,7 @@
 
    with procedure Read (Buf : out Buffer_Type; Len : out Natural);
 
-package FS.FILO.VFS
-with
-   SPARK_Mode => Off,
-   Convention => C
-is
+package FS.FILO.VFS is
 
    function C_Mount return int;