# HG changeset patch
# User haftmann
# Date 1389424212 -3600
# Node ID 3f561ee3d9988462049382d51a3e48197a6d608d
# Parent  fe454ca3405f43678cc9f1720dc7cc6e12ac6020
dropped legacy alias feature

diff -r fe454ca3405f -r 3f561ee3d998 src/Tools/Code/code_target.ML
--- 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 =