src/Doc/System/Phabricator.thy

   \<^medskip>
   Mailer configuration requires a few command-line invocations as follows:
 
   @{verbatim [display] \<open>  isabelle phabricator_setup_mail\<close>}
 
-  \<^noindent> This generates a JSON template file for the the mail account details.
+  \<^noindent> This generates a JSON template file for the mail account details.
   After editing that, the subsequent command will add and test it with
   Phabricator:
 
   @{verbatim [display] \<open>  isabelle phabricator_setup_mail -T makarius\<close>}