mysql_option

type mysql_option = (

  MYSQL_OPT_CONNECT_TIMEOUT,

  MYSQL_OPT_COMPRESS,

  MYSQL_OPT_NAMED_PIPE,

  MYSQL_INIT_COMMAND,

  MYSQL_READ_DEFAULT_FILE,

  MYSQL_READ_DEFAULT_GROUP,

  MYSQL_SET_CHARSET_DIR,

  MYSQL_SET_CHARSET_NAME

);