changeset 54987 | 3f561ee3d998 |
parent 54890 | cb892d835803 |
child 55146 | 525309c2e4ee |
--- 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 =