[m-rev.] for review: Allow remove_file to remove an empty dir on C# backend.
novalazy at gmail.com
Fri Aug 26 15:08:32 AEST 2022
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
For C#, previously it didn't, now it will.
> These documentation changes should be reflect in the obsolete version in
Will do, thanks.
More information about the reviews