ADDED: delete_file/1, addressing a remaining aspect of #511

2020-07-14 22:16:15 +02:00
parent 53d39ccb4b
commit 5134e64cae
3 changed files with 18 additions and 0 deletions
--- a/src/lib/files.pl
+++ b/src/lib/files.pl
@@ -50,6 +50,7 @@
                  file_size/2,
                  file_exists/1,
                  directory_exists/1,
+                  delete_file/1,
                  make_directory/1]).

 :- use_module(library(error)).
@@ -80,3 +81,7 @@ directory_exists(Directory) :-
 make_directory(Directory) :-
        list_of_chars(Directory),
        '$make_directory'(Directory).
+
+delete_file(File) :-
+        list_of_chars(File),
+        '$delete_file'(File).