فهرست منبع

reset use_parser_resume to true for normal completion every time (closes #3324)

Dan Korostelev 11 سال پیش
والد
کامیت
304f6d2a1e
1فایلهای تغییر یافته به همراه1 افزوده شده و 0 حذف شده
  1. 1 0
      main.ml

+ 1 - 0
main.ml

@@ -1192,6 +1192,7 @@ try
 						activate_special_display_mode();
 						activate_special_display_mode();
 						DMToplevel
 						DMToplevel
 					| _ ->
 					| _ ->
+						Parser.use_parser_resume := true;
 						DMDefault
 						DMDefault
 				in
 				in
 				let pos = try int_of_string pos with _ -> failwith ("Invalid format : "  ^ pos) in
 				let pos = try int_of_string pos with _ -> failwith ("Invalid format : "  ^ pos) in