public class Filenames
extends java.lang.Object
Constructor and Description |
---|
Filenames() |
Modifier and Type | Method and Description |
---|---|
static java.util.List<java.lang.String> |
disectFilename(java.lang.String filename)
Separates the single directory entries in a filename.
|
static java.lang.String |
makeFilenameRelative(java.lang.String origFilename,
java.lang.String toFilename)
Returns a filename relative to another one.
|
static java.lang.String |
toValidFileName(java.lang.String s) |
public static java.util.List<java.lang.String> disectFilename(java.lang.String filename)
public static java.lang.String makeFilenameRelative(java.lang.String origFilename, java.lang.String toFilename)
public static java.lang.String toValidFileName(java.lang.String s)
Copyright © 2003-2019 The KeY-Project.