shared_files = []

(*
 The following options are not used (errors, obsolete, ...) 
*)