diff options
| author | Maxime Dénès | 2017-06-02 14:35:13 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-02 14:35:13 +0200 |
| commit | 13e8983e3be6bff993c212d7fdcf707cf3c749c6 (patch) | |
| tree | 46ad587ecdbf12e7cd047e9f2029b81db347a9c2 /stm | |
| parent | 129faf2dbd68e0f3ab8688496372b6406e3ee2e4 (diff) | |
| parent | 6b041a242607ec906fbab451e53c15af6339e4ef (diff) | |
Merge PR#647: [emacs] [toplevel] Make emacs flag local to the toplevel.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index b98cb312ed..2057496f4b 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -66,7 +66,7 @@ end (* During interactive use we cache more states so that Undoing is fast *) let interactive () = - if !Flags.ide_slave || !Flags.print_emacs || not !Flags.batch_mode then `Yes + if !Flags.ide_slave || not !Flags.batch_mode then `Yes else `No let async_proofs_workers_extra_env = ref [||] @@ -1094,7 +1094,7 @@ end = struct (* {{{ *) VtStm (VtBack oid, true), VtLater | VernacBacktrack (id,_,_) | VernacBackTo id -> - VtStm (VtBack (Stateid.of_int id), not !Flags.print_emacs), VtNow + VtStm (VtBack (Stateid.of_int id), not !Flags.batch_mode), VtNow | _ -> VtUnknown, VtNow with | Not_found -> |