[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