function dot_msg {
  echo "$@"
}