#101 Remove idrename
Metadata
Property | Value |
---|---|
Reported by | Oliver Sander (oliver.sander@tu-dresden.de) |
Reported at | Feb 17, 2006 10:31 |
Type | Feature Request |
Version | Git (pre2.4) [autotools] |
Operating System | Unspecified / All |
Closed by | Christian Engwer (christi@conan.iwr.uni-heidelberg.de) |
Closed at | Jul 12, 2006 08:26 |
Closed in version | Unknown |
Resolution | Fixed |
Comment |
Description
The program idrename (in dune/bin) is certainly a helpful programming tool. However, it is not Dune-specific, and it is not documented at all. In fact, in the rare cases where we need a large-scale renaming I'd still rather do it by hand, because I don't really know precisely what idrename is doing. For all those reasons I suggest we remove idrename from Dune.