java.io.File: "normalize" path names

[Per Bothner]

Bryce McKinlay <bryce@albatross.co.nz> writes:

> Path names represented by File objects should not contain "any
> duplicate or redundant separator characters". This patch "normalizes"
> File paths which contain such characters, consistent with the JDK.

There is also code in java/net/URLStreamHandler.java (parseURL)
to normalize URLs.  I'm skeptical as to whether that's a good idea,
but I don't know if JDK does the same.
-- 
	--Per Bothner
per@bothner.com   http://www.bothner.com/~per/