From 5d2d2d270d706345fb758f0db86e77f4f8cd8eff Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Thu, 20 Aug 2009 09:42:40 +0000
Subject: [PATCH] Build bytecode version with debug symbols.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1135 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 Makefile | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Makefile b/Makefile
index e82d2054d..f9abb5301 100644
--- a/Makefile
+++ b/Makefile
@@ -97,8 +97,8 @@ ccomp: driver/Configuration.ml
         && rm -f ccomp && ln -s _build/driver/Driver.native ccomp
 
 ccomp.byte: driver/Configuration.ml
-	$(OCAMLBUILD) $(OCB_OPTIONS) Driver.byte \
-        && rm -f ccomp.byte && ln -s _build/driver/Driver.byte ccomp.byte
+	$(OCAMLBUILD) $(OCB_OPTIONS) Driver.d.byte \
+        && rm -f ccomp.byte && ln -s _build/driver/Driver.d.byte ccomp.byte
 
 runtime:
 	$(MAKE) -C runtime
-- 
GitLab