Merge pull request #609 from coq-community/error-backtrace

Remove backtrace from errors by default
coq · Sep 4, 2023 · dead809 · dead809
2 parents ef34537 + f9677f4
commit dead809
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 2 deletions.
diff --git a/client/search-ui/src/components/atoms/Error.tsx b/client/search-ui/src/components/atoms/Error.tsx
@@ -16,7 +16,7 @@ const error: FunctionComponent<ErrorProps> = (props) => {
 
     return (
         <div className={classes.Error}>
-            <span className={classes.ErrorHeader}> Error {error.code} </span>
+            <span className={classes.ErrorHeader}> Error </span>
             <span className={classNames.join(' ')}> {error.message} </span>
         </div>
     );

diff --git a/language-server/vscoqtop/vscoqtop.ml b/language-server/vscoqtop/vscoqtop.ml
@@ -75,5 +75,4 @@ let _ =
   Safe_typing.allow_delayed_constants := true; (* Needed to delegate or skip proofs *)
   Flags.quiet := true;
   Sys.(set_signal sigint Signal_ignore);
-  Exninfo.record_backtrace true;
   loop injections