changeset 51945 | 5b1ac9843f02 |
parent 51943 | 3278729bfa38 |
child 51946 | 449fbf64f4a5 |
--- a/src/Pure/System/options.ML Sun May 12 17:51:34 2013 +0200 +++ b/src/Pure/System/options.ML Sun May 12 17:56:53 2013 +0200 @@ -1,7 +1,7 @@ (* Title: Pure/System/options.ML Author: Makarius -Stand-alone options with external string representation. +System options with external string representation. *) signature OPTIONS =