equal
deleted
inserted
replaced
20 end |
20 end |
21 *} |
21 *} |
22 |
22 |
23 setup {* Code_Target.set_default_code_width 74 *} |
23 setup {* Code_Target.set_default_code_width 74 *} |
24 |
24 |
25 ML_command {* unique_names := false *} |
25 declare [[unique_names = false]] |
26 |
26 |
27 end |
27 end |