X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=modules%2Fstdint;h=c11825a12e46103d0d7e23293330d939dfb0c8b1;hb=76d82d2d7f5ba1a69da6aaa71ff170f5a90a6c94;hp=2878da6d32e1830a823ba180fc294deab62a31d7;hpb=b4b6391081d1173278396afdf098be68b1768752;p=pspp

diff --git a/modules/stdint b/modules/stdint
index 2878da6d32..c11825a12e 100644
--- a/modules/stdint
+++ b/modules/stdint
@@ -23,6 +23,7 @@ BUILT_SOURCES += $(STDINT_H)
 
 # We need the following in order to create <stdint.h> when the system
 # doesn't have one that works with the given compiler.
+if GL_GENERATE_STDINT_H
 stdint.h: stdint.in.h $(top_builddir)/config.status
 	$(AM_V_GEN)rm -f $@-t $@ && \
 	{ echo '/* DO NOT EDIT! GENERATED AUTOMATICALLY! */'; \
@@ -55,6 +56,10 @@ stdint.h: stdint.in.h $(top_builddir)/config.status
 	      < $(srcdir)/stdint.in.h; \
 	} > $@-t && \
 	mv $@-t $@
+else
+stdint.h: $(top_builddir)/config.status
+	rm -f $@
+endif
 MOSTLYCLEANFILES += stdint.h stdint.h-t
 
 Include: