On 64-bit systems dINT is used instead of INT.

bec32129 · Arjan Oortgiese · b7e8c32c · bec32129
Commit bec32129 authored Sep 23, 2016 by Arjan Oortgiese
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 1 deletion

common/graph_copy_with_names.icl common/graph_copy_with_names.icl +1 -1

No files found.
--- a/common/graph_copy_with_names.icl
+++ b/common/graph_copy_with_names.icl
@@ -336,7 +336,7 @@ get_thunk_n_non_pointers d
 make_symbol_name "_system" descriptor_name prefix
 	= case descriptor_name of {
 		"INT"
-			-> descriptor_name;
+			-> IF_INT_64_OR_32 "dINT" descriptor_name;
 		"CHAR"
 			-> descriptor_name;
 		"REAL"