method get_slice_name () = slice_name
(** A new script was copied into the backend, make a corresponding entry in
the frontend.
method get_slice_name () = slice_name
(** A new script was copied into the backend, make a corresponding entry in
the frontend.