patch 8.0.0949: winpty.dll name is fixed
Problem: winpty.dll name is fixed.
Solution: Add the 'winptydll' option. Make the default name depend on
whether it is a 32-bit or 64-bit build. (idea by Yasuhiro
Matsumoto, closes #1978)
diff --git a/src/option.h b/src/option.h
index 9b7e88f..b772a8e 100644
--- a/src/option.h
+++ b/src/option.h
@@ -966,6 +966,9 @@
EXTERN long p_wmw; /* 'winminwidth' */
EXTERN long p_wiw; /* 'winwidth' */
#endif
+#if defined(WIN3264) && defined(TERMINAL)
+EXTERN char_u *p_winptydll; /* 'winptydll' */
+#endif
EXTERN int p_ws; /* 'wrapscan' */
EXTERN int p_write; /* 'write' */
EXTERN int p_wa; /* 'writeany' */