Revision 110:125520c3dc05 repoint

View differences:

repoint
58 58 
    # That is fixed in v5.7.1, so we could promote it up the order
59 59 
    # again at some point in future
60 60 
    elif echo | poly -v 2>/dev/null | grep -q 'Poly/ML'; then
61 
	sml="poly"
61 
	sml="polyml"
62 62 
    elif mlton 2>&1 | grep -q 'MLton'; then
63 63 
	sml="mlton"
64 64 
    # MLKit is at the bottom because it leaves compiled files around
......
109 109 
done
110 110 

  		




  111
  111
  
    
case "$sml" in


  		




  112
  
  
    
    poly)


  		




  
  112
  
    
    polyml)


  		




  113
  113
  
    
        if [ -n "$local_install" ] && polyc --help >/dev/null 2>&1 ; then


  		




  114
  114
  
    
            if [ ! -x "$gen_out" ]; then


  		




  115
  115
  
    
                polyc -o "$gen_out" "$program"


  		












Also available in:  Unified diff