| changeset 69427 | ff2f39a221d4 |
| parent 69300 | 8b6ab9989bcd |
| child 69483 | 023d92df3d84 |
--- a/src/Pure/General/file.ML Sat Dec 08 15:13:28 2018 +0100 +++ b/src/Pure/General/file.ML Sat Dec 08 21:13:47 2018 +0100 @@ -117,7 +117,7 @@ | SOME entry => read (f entry x)); in read a end); -fun read_dir path = rev (fold_dir cons path []); +fun read_dir path = sort_strings (fold_dir cons path []); (* input *)