Choice of backslash as escape character conflicted on Windows.
Changed to pipe '|'. M src/edu/rice/cs/drjava/config/VectorOption.java M src/edu/rice/cs/drjava/config/VectorOptionTest.java
Authored by: mgricken 2008-02-19
Parent: [r4348]
Child: [r4350]