From bd85aba84475dd956af21c461c44a584958099d1 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 14 Jul 2012 08:05:36 +0000
Subject: Support for indirect symbols under MacOS X (final). Remove stdio hack
 in runtime/

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1979 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 runtime/Makefile |  8 ++++----
 runtime/stdio.c  | 23 -----------------------
 runtime/stdio.h  | 35 -----------------------------------
 3 files changed, 4 insertions(+), 62 deletions(-)
 delete mode 100644 runtime/stdio.c
 delete mode 100644 runtime/stdio.h

(limited to 'runtime')

diff --git a/runtime/Makefile b/runtime/Makefile
index ef8e21b..c128ba2 100644
--- a/runtime/Makefile
+++ b/runtime/Makefile
@@ -1,11 +1,11 @@
 include ../Makefile.config
 
 CFLAGS=-O1 -g -Wall
-OBJS=stdio.o
+INCLUDES=
+OBJS=
 LIB=libcompcert.a
-INCLUDES=stdio.h
 
-ifeq ($(strip $(NEED_STDLIB_WRAPPER)),true)
+ifeq ($(strip $(HAS_RUNTIME_LIB)),true)
 all: $(LIB) $(INCLUDES)
 else
 all:
@@ -18,7 +18,7 @@ $(LIB): $(OBJS)
 clean:
 	rm -f *.o $(LIB)
 
-ifeq ($(strip $(NEED_STDLIB_WRAPPER)),true)
+ifeq ($(strip $(HAS_RUNTIME_LIB)),true)
 install:
 	install -d $(LIBDIR)
 	install -c $(LIB) $(INCLUDES) $(LIBDIR)
diff --git a/runtime/stdio.c b/runtime/stdio.c
deleted file mode 100644
index 881a7fa..0000000
--- a/runtime/stdio.c
+++ /dev/null
@@ -1,23 +0,0 @@
-/* *********************************************************************/
-/*                                                                     */
-/*              The Compcert verified compiler                         */
-/*                                                                     */
-/*          Xavier Leroy, INRIA Paris-Rocquencourt                     */
-/*                                                                     */
-/*  Copyright Institut National de Recherche en Informatique et en     */
-/*  Automatique.  All rights reserved.  This file is distributed       */
-/*  under the terms of the GNU General Public License as published by  */
-/*  the Free Software Foundation, either version 2 of the License, or  */
-/*  (at your option) any later version.  This file is also distributed */
-/*  under the terms of the INRIA Non-Commercial License Agreement.     */
-/*                                                                     */
-/* *********************************************************************/
-
-/* Thin wrapper around stdio, redefining stdin, stdout and stderr.
-   Needed under MacOS X because of linking issues with dynamic libraries. */
-
-#include "/usr/include/stdio.h"
-
-FILE * compcert_stdin(void)  { return stdin; }
-FILE * compcert_stdout(void) { return stdout; }
-FILE * compcert_stderr(void) { return stderr; }
diff --git a/runtime/stdio.h b/runtime/stdio.h
deleted file mode 100644
index daf0198..0000000
--- a/runtime/stdio.h
+++ /dev/null
@@ -1,35 +0,0 @@
-/* *********************************************************************/
-/*                                                                     */
-/*              The Compcert verified compiler                         */
-/*                                                                     */
-/*          Xavier Leroy, INRIA Paris-Rocquencourt                     */
-/*                                                                     */
-/*  Copyright Institut National de Recherche en Informatique et en     */
-/*  Automatique.  All rights reserved.  This file is distributed       */
-/*  under the terms of the GNU General Public License as published by  */
-/*  the Free Software Foundation, either version 2 of the License, or  */
-/*  (at your option) any later version.  This file is also distributed */
-/*  under the terms of the INRIA Non-Commercial License Agreement.     */
-/*                                                                     */
-/* *********************************************************************/
-
-/* Thin wrapper around stdio, redefining stdin, stdout and stderr.
-   Needed under MacOS X because of linking issues with dynamic libraries. */
-
-#ifndef _COMPCERT_STDIO_H
-#define _COMPCERT_STDIO_H
-
-#include "/usr/include/stdio.h"
-
-extern FILE * compcert_stdin(void);
-extern FILE * compcert_stdout(void);
-extern FILE * compcert_stderr(void);
-
-#undef stdin
-#define stdin (compcert_stdin())
-#undef stdout
-#define stdout (compcert_stdout())
-#undef stderr
-#define stderr (compcert_stderr())
-
-#endif
-- 
cgit v1.2.3