[m-rev.] for review: Allow remove_file to remove an empty dir on C# backend.

[Peter Wang]

Do we want to define remove_file to removing empty directories?

-----

library/io.file.m:
    Change the C# implementation of remove_file to delete empty
    directories.

    Document that remove_file may delete empty directories.

diff --git a/library/io.file.m b/library/io.file.m
index a9a86fb8c..8401a7e36 100644
--- a/library/io.file.m
+++ b/library/io.file.m
@@ -28,6 +28,10 @@
     % fails. If FileName names a file that is currently open, the behaviour
     % is implementation-dependent.
     %
+    % If FileName names a directory, the behavior is currently
+    % implementation-dependent. On most platforms, an empty directory will be
+    % deleted.
+    %
 :- pred remove_file(string::in, io.res::out, io::di, io::uo) is det.
 
     % remove_file_recursively(FileName, Result, !IO) attempts to remove
@@ -243,6 +247,7 @@ remove_file(FileName, Result, !IO) :-
 "
     int rc;
 #ifdef MR_WIN32
+    // XXX _wremove will not delete an empty directory; _wrmdir does that.
     rc = _wremove(ML_utf8_to_wide(FileName));
 #else
     rc = remove(FileName);
@@ -261,13 +266,13 @@ remove_file(FileName, Result, !IO) :-
     try {
         // System.IO.File.Delete() does not throw an exception
         // if the file does not exist.
-        // XXX This won't delete an empty directory unlike the C and Java
-        // implementations.
         if (System.IO.File.Exists(FileName)) {
             System.IO.File.Delete(FileName);
             Error = null;
+        } else if (System.IO.Directory.Exists(FileName)) {
+            System.IO.Directory.Delete(FileName);
+            Error = null;
         } else {
-            // This is a bit misleading if FileName names a directory.
             Error = new System.IO.FileNotFoundException();
         }
     }
-- 
2.37.1