(******************************************************************************)
(* this should be the only hard coded constant *)
(******************************************************************************)
(* this should be the only hard coded constant *)