src/Pure/General/file.scala
changeset 62704 478b49f0d726
parent 62703 01b71da798dd
child 62829 4141c2a8458b
     1.1 --- a/src/Pure/General/file.scala	Thu Mar 24 13:22:02 2016 +0100
     1.2 +++ b/src/Pure/General/file.scala	Thu Mar 24 14:55:43 2016 +0100
     1.3 @@ -264,14 +264,4 @@
     1.4    }
     1.5  
     1.6    def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file)
     1.7 -
     1.8 -
     1.9 -  /* approximative time stamp */
    1.10 -
    1.11 -  def time_stamp(path: Path): Option[String] =
    1.12 -  {
    1.13 -    val file = path.file
    1.14 -    if (file.isFile) Some(file.length.toString + " " + file.lastModified.toString)
    1.15 -    else None
    1.16 -  }
    1.17  }