From c1639b3e527e89e8199fafebfd4ff8e55b7f092c Mon Sep 17 00:00:00 2001
From: Anatol Belski <ab@php.net>
Date: Sat, 25 Oct 2014 13:01:17 +0200
Subject: [PATCH] stdint will be included in the win32 variant, so don't do it
 twice

---
 phpdbg.h | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/phpdbg.h b/phpdbg.h
index 8c0dbb4afa..4147198b3d 100644
--- a/phpdbg.h
+++ b/phpdbg.h
@@ -29,8 +29,12 @@
 # define PHPDBG_API
 #endif
 
-#include <stdint.h>
-#include <stddef.h>
+#ifndef PHP_WIN32
+#	include <stdint.h>
+#	include <stddef.h>
+#else
+#	include "win32/php_stdint.h"
+#endif
 #include "php.h"
 #include "php_globals.h"
 #include "php_variables.h"
@@ -50,7 +54,6 @@
 #if defined(_WIN32) && !defined(__MINGW32__)
 #	include <windows.h>
 #	include "config.w32.h"
-#	include "win32/php_stdint.h"
 #	undef  strcasecmp
 #	undef  strncasecmp
 #	define strcasecmp _stricmp 
-- 
2.50.0