On Tuesday, November 27, 2007, at 01:24PM, "Ketil Malde" wrote: >Ben Franksen writes: >.. This would let you have different files >with the same name at different times.
The problem I have with ghosts of deleted files is precisely that once a file is deleted, a new file can never be created with the same name. Ugh. --Doug _______________________________________________ darcs-users mailing list [email protected] http://lists.osuosl.org/mailman/listinfo/darcs-users
