[darcs-users] deleting a repository

Albert Reiner areiner at tph.tuwien.ac.at
Mon Aug 22 13:28:17 UTC 2005


[Martin Ellis <m.a.ellis at ncl.ac.uk>, Mon, 22 Aug 2005 13:49:38 +0100]:
> > - When operating on the current repo, I can see two options:
> >
> >   - leave the user in a different directory; most likely, the one
> >     above the root of the repo;
> 
> I don't think this is an option.

Well, it is an option on Unix, provided it is a script and not a darcs
command.  That was the point I was trying to make, and is part of the
reason why I think it should emphatically not be a darcs command.

It's uselessness being the main reason, of course.

Regards,

Albert.




More information about the darcs-users mailing list