changeset 28021:8933b2985dd5

maint: merge stable to default.
author Kai T. Ohlhus <k.ohlhus@gmail.com>
date Tue, 28 Jan 2020 11:00:09 +0900
parents c45a0d7e9385 (current diff) eb46a9f47164 (diff)
children 306df6825dd9
files scripts/miscellaneous/mkoctfile.m
diffstat 1 files changed, 5 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/scripts/miscellaneous/mkoctfile.m	Mon Jan 27 10:34:00 2020 -0800
+++ b/scripts/miscellaneous/mkoctfile.m	Tue Jan 28 11:00:09 2020 +0900
@@ -219,6 +219,11 @@
   endif
 
   cmd = ['"' shell_script '"'];
+  if (ispc () && isguirunning ())
+    ## FIXME: Remove this branch when the MS Windows GUI terminal widget can
+    ##        properly handle colors (bug #57658).
+    cmd = [cmd ' "-fdiagnostics-color=never"'];
+  endif
   for i = 1:nargin
     cmd = [cmd ' "' varargin{i} '"'];
   endfor