|
From: <sv...@va...> - 2007-11-09 15:44:27
|
Author: sewardj Date: 2007-11-09 15:44:15 +0000 (Fri, 09 Nov 2007) New Revision: 7113 Log: Rename this directory. Added: trunk/old-helgrind/ Removed: trunk/helgrind/ Copied: trunk/old-helgrind (from rev 7110, trunk/helgrind) |
|
From: Nicholas N. <nj...@cs...> - 2007-11-09 22:39:27
|
On Fri, 9 Nov 2007 sv...@va... wrote: > Author: sewardj > Date: 2007-11-09 15:44:15 +0000 (Fri, 09 Nov 2007) > New Revision: 7113 > > Log: > Rename this directory. > > Added: > trunk/old-helgrind/ > Removed: > trunk/helgrind/ Will you delete this eventually? Nick |
|
From: Julian S. <js...@ac...> - 2007-11-09 23:36:52
|
> > Added: > > trunk/old-helgrind/ > > Removed: > > trunk/helgrind/ > > Will you delete this eventually? Yes, providing that's OK with you & Jeremy. Or can leave it around for reference purposes. J |
|
From: Nicholas N. <nj...@cs...> - 2007-11-10 00:25:14
|
On Sat, 10 Nov 2007, Julian Seward wrote: >> Will you delete this eventually? > > Yes, providing that's OK with you & Jeremy. Or can leave it around > for reference purposes. I say delete. It's still in the repo and old releases anyway. N |