Project

General

Profile

« Previous | Next » 

Revision b8ae1bbc

Added by Pierre-Loïc Garoche almost 9 years ago

Improvements as suggested by e. Noulard: better install of include; modified generated makefile

View differences:

src/c_backend.ml
28 28 
open Corelang
29 29 
open Machine_code
30 30 

  		




  31
  
  
    

  		




  32
  31
  
    
(********************************************************************************************)


  		




  33
  32
  
    
(*                     Basic      Printing functions                                        *)


  		




  34
  33
  
    
(********************************************************************************************)


  		




  ......




  772
  771
  
    

  		




  773
  772
  
    
let print_makefile basename nodename fmt =


  		




  774
  773
  
    
  fprintf fmt "GCC=gcc@.";


  		




  775
  
  
    
  fprintf fmt "INC=/usr/local/include/lustrec@.";


  		




  
  774
  
    
  fprintf fmt "LUSTREC=%s@." Sys.executable_name;


  		




  
  775
  
    
  fprintf fmt "LUSTREC_BASE=%s@." (Filename.dirname (Filename.dirname Sys.executable_name));


  		




  
  776
  
    
  fprintf fmt "INC=${LUSTREC_BASE}/include/lustrec@.";


  		




  776
  777
  
    
  fprintf fmt "@.";


  		




  777
  778
  
    
  fprintf fmt "%s_%s:@." basename nodename;


  		




  778
  779
  
    
  fprintf fmt "\t${GCC} -I${INC} -I. -c %s.c@." basename;    


  		




  779
  780
  
    
  fprintf fmt "\t${GCC} -I${INC} -c ${INC}/io_frontend.c@.";    


  		




  780
  781
  
    
(*  fprintf fmt "\t${GCC} -I${INC} -c ${INC}/StdLibrary.c@."; *)


  		




  781
  782
  
    
(*  fprintf fmt "\t${GCC} -o %s_%s io_frontend.o StdLibrary.o -lm %s.o@." basename nodename basename*)


  		




  782
  
  
    
 fprintf fmt "\t${GCC} -o %s_%s io_frontend.o -lm %s.o@." basename nodename basename


  		




  
  783
  
    
 fprintf fmt "\t${GCC} -o %s_%s io_frontend.o -lm %s.o@." basename nodename basename;


  		




  
  784
  
    
 fprintf fmt "@.";


  		




  
  785
  
    
 fprintf fmt "clean:@.";


  		




  
  786
  
    
 fprintf fmt "\t\\rm -f *.o %s_%s@." basename nodename


  		




  783
  787
  
    

  		




  784
  788
  
    

  		




  785
  789
  
    

  		












Also available in:  Unified diff