summaryrefslogtreecommitdiff
path: root/runtime/Makefile
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-04-23 09:18:37 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-04-23 09:18:37 +0000
commit4d78351d21f8a52c4b64313354f24dd534205256 (patch)
treef562e1ac1eb953e09a0acfccd275ba706e16521b /runtime/Makefile
parent945e1e3c0e601f711ab83f65333f4c2b9e713c99 (diff)
Make ia32/ code more portable across systems.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2214 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'runtime/Makefile')
-rw-r--r--runtime/Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/runtime/Makefile b/runtime/Makefile
index 6f45850..3565fb1 100644
--- a/runtime/Makefile
+++ b/runtime/Makefile
@@ -17,7 +17,7 @@ $(LIB): $(OBJS)
$(CASMRUNTIME) $^
%.o: $(ARCH)/%.S
- $(CASMRUNTIME) -DVARIANT_$(VARIANT) $^
+ $(CASMRUNTIME) -DVARIANT_$(VARIANT) -DSYS_$(SYSTEM) $^
clean::
rm -f *.o $(LIB)