push_int


Description:

public void push_int (string symbol, long value)