a8bd67e Merge revert of "Modify BigInts due to the bug in FF linter"

Merged and Committed by Libor Polčák 3 years ago
    Merge revert of "Modify BigInts due to the bug in FF linter"
    
    No longer needed