changeset 68808 | 5467858e9419 |
parent 68292 | 7ca0c23179e6 |
child 69349 | 7cef9e386ffe |
--- a/src/Pure/Thy/sessions.ML Sat Aug 25 20:22:00 2018 +0200 +++ b/src/Pure/Thy/sessions.ML Sat Aug 25 20:48:16 2018 +0200 @@ -37,7 +37,7 @@ val export_files = Parse.$$$ "export_files" |-- - Parse.!!! (Scan.optional in_path ("export", Position.none) -- Scan.repeat1 Parse.name); + Parse.!!! (Scan.optional in_path ("export", Position.none) -- Scan.repeat1 Parse.embedded); in