Valery,
I implemented your idea in cint5.14.3. Cint tmpfiles are named ???_cint
for all platforms. It is OK to remove those files by *_cint unless of course
you do not have any important file with the similar name.
Thank you
Masaharu Goto
==========================================================================
Hello, Masa
I'd like to mention it is quite complicate under Windows since the name of
those
files are a "pure" numbers, like "23" "45" "12" etc.
This entails one can not apply any reg expression to delete all of them at
once but "*".
Is it possible to supply any extension as well like "Cint". So I can remove
them as follows:
del /tmp/*.Cint
With my regards,
Valery
This archive was generated by hypermail 2b29 : Tue Jan 04 2000 - 00:43:33 MET