Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
dropped legacy alias feature
authorhaftmann
Sat, 11 Jan 2014 08:10:12 +0100
changeset 54987 3f561ee3d998
parent 54986 fe454ca3405f
child 54988 f3b6f80cc15d
dropped legacy alias feature
src/Tools/Code/code_target.ML file | annotate | diff | comparison | revisions 
--- a/src/Tools/Code/code_target.ML	Fri Jan 10 23:44:03 2014 +0100
+++ b/src/Tools/Code/code_target.ML	Sat Jan 11 08:10:12 2014 +0100
@@ -511,7 +511,6 @@
   in union (op =) cs3 cs1 end;
 
 fun prep_destination "" = NONE
-  | prep_destination "-" = (legacy_feature "drop \"file\" argument entirely instead of \"-\""; NONE)
   | prep_destination s = SOME (Path.explode s);
 
 fun export_code thy cs seris =
isabelle