r208380 - Fix filename in file header comment.

[Jonathan Roelofs]

On 5/8/14, 6:44 PM, Rafael Espíndola wrote:
>> I thought the point of those headers was for when people (read: lawyers)
>> print out the source. In that case I could see having the file name in
>> the comment being useful.
>
> I thought that every editor had the option of including the file name
> as a page header in print, no?
Good point.
>
> Cheers,
> Rafael
>

-- 
Jon Roelofs
jonathan at codesourcery.com
CodeSourcery / Mentor Embedded