HANDLE2FILENAME Convert an integer file handle to a filename

Contents

Inputs

Outputs