diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-04-23 09:18:37 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-04-23 09:18:37 +0000 |
commit | 4d78351d21f8a52c4b64313354f24dd534205256 (patch) | |
tree | f562e1ac1eb953e09a0acfccd275ba706e16521b /runtime/Makefile | |
parent | 945e1e3c0e601f711ab83f65333f4c2b9e713c99 (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/Makefile | 2 |
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) |