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

[Peter Wang]

On Fri, 26 Aug 2022 12:44:08 +1000 Julien Fischer <jfischer at opturion.com> wrote:
> 
> On Thu, 25 Aug 2022, Peter Wang wrote:
> 
> > Do we want to define remove_file to removing empty directories?
> 
> The documentation for remove_file_recursively suggests that was
> intended to be the case.
> 
>      % Unlike remove_file, this predicate will attempt to remove non-empty
>      % directories (recursively). If it fails, some of the directory
>      % elements may already have been removed.
> 

Probably. But it actually only talks about non-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.
> > +    %
> 
> Is the only platform where it is now not delete any empty directory
> Windows (i.e the XXX below)?

Yes, assuming other OSs follow POSIX.

For Java, the java.io.File.delete() method is specified to delete an
empty directory.

For C#, previously it didn't, now it will.

> 
> These documentation changes should be reflect in the obsolete version in
> io.m.

Will do, thanks.

Peter