[ptp-dev] Git and case insensitive filesystems

[Greg Watson <g.watson@xxxxxxxxxxxx>]

It looks like Git can't handle case insensitive filesystems correctly.

There were two html files with the same name apart from the case (allindex.html and allIndex.html) in the org.eclipse.ptp.pldt.mpi.core plugin in the ptp_5_0 branch. This was causing me grief because git was only able to check one of them out, so it always thought that I'd deleted the second. I ended up removing the lowercase one. I'm not sure if this has broken anything. Please check.

Greg