Skip to content

Commit

Permalink
test to see if fmt works
Browse files Browse the repository at this point in the history
  • Loading branch information
ejgallego committed Mar 6, 2023
1 parent fb15902 commit 81b61e6
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 6 deletions.
4 changes: 1 addition & 3 deletions controller-js/coq_lsp_worker.ml
Original file line number Diff line number Diff line change
Expand Up @@ -81,9 +81,7 @@ let setup_std_printers () =

external coq_vm_trap : unit -> unit = "coq_vm_trap"

let post_message (json : Yojson.Safe.t) =
let js = json_to_obj (Js.Unsafe.obj [||]) json in
Worker.post_message js
let post_message (json : Yojson.Safe.t) = let js = json_to_obj (Js.Unsafe.obj [||]) json in Worker.post_message js

external interrupt_setup : opaque (* Uint32Array *) -> unit = "interrupt_setup"

Expand Down
4 changes: 1 addition & 3 deletions editor/code/lib/types.ts
Original file line number Diff line number Diff line change
Expand Up @@ -57,9 +57,7 @@ export interface OblsView {
export type ProgramInfo = [Id, OblsView][];

export interface GoalAnswer<Pp> {
textDocument: VersionedTextDocumentIdentifier;
position: Position;
goals?: GoalConfig<Pp>;
textDocument: VersionedTextDocumentIdentifier; position: Position; goals?: GoalConfig<Pp>;
program?: ProgramInfo;
messages: Pp[] | Message<Pp>[];
error?: Pp;
Expand Down

0 comments on commit 81b61e6

Please sign in to comment.