/src/Doc/JEdit/document/
drwxr-xr-x [up]
-rw-r--r-- 2014-04-05 15:03 +0200 41671 auto-tools.png
-rwxr-xr-x 2014-04-05 15:03 +0200 439 build
-rw-r--r-- 2014-04-05 15:03 +0200 60874 find.png
-rw-r--r-- 2014-04-05 15:03 +0200 100951 isabelle-jedit.png
-rw-r--r-- 2014-04-05 15:03 +0200 115600 output.png
-rw-r--r-- 2014-04-05 15:03 +0200 23987 popup1.png
-rw-r--r-- 2014-04-05 15:03 +0200 33951 popup2.png
-rw-r--r-- 2014-04-05 15:03 +0200 2141 root.tex
-rw-r--r-- 2014-04-05 15:03 +0200 66822 sledgehammer.png