Re: new json, push generated file?

From:	Jan Ehrhardt	Date:	Mon, 09 Feb 2015 07:48:53 +0000
Subject:	Re: new json, push generated file?
References:	1	Groups:	php.internals
Request:	Send a blank email to [email protected] to get a copy of this message

Pierre Joye in php.internals (Mon, 9 Feb 2015 09:40:21 +0700):
>Should we push json_parser.tab.c? Which is generated (re2c), just like
>what is done in date or other?

Yes, you should. I ran into this problem when I tried to compile PHP7
from git head. The Windows builds are currently broken:
http://windows.php.net/downloads/snaps/master/r0698901/logs/make-nts-windows-vc11-x86-r0698901.html

Jan


   

Thread (24 messages)

• Pierre JoyeMon, 09 Feb 2015 02:40:21 +0000
  • Stanislav MalyshevMon, 09 Feb 2015 03:45:19 +0000
  • Xinchen HuiMon, 09 Feb 2015 04:10:48 +0000
    • Pierre JoyeMon, 09 Feb 2015 05:44:57 +0000
      • Xinchen HuiMon, 09 Feb 2015 06:33:29 +0000
        • Anatol BelskiMon, 09 Feb 2015 09:18:15 +0000
          • Jakub ZelenkaMon, 09 Feb 2015 09:46:04 +0000
            • Pierre JoyeMon, 09 Feb 2015 13:55:36 +0000
              • Jakub ZelenkaMon, 09 Feb 2015 19:19:18 +0000
                • Xinchen HuiTue, 10 Feb 2015 02:47:36 +0000
                  • Pierre JoyeTue, 10 Feb 2015 03:02:28 +0000
                  • Jakub ZelenkaTue, 10 Feb 2015 11:56:09 +0000
                    • Anatol BelskiTue, 10 Feb 2015 12:24:35 +0000
                      • Jakub ZelenkaTue, 10 Feb 2015 13:15:50 +0000
                        • Anatol BelskiTue, 10 Feb 2015 15:35:02 +0000
                          • Jakub ZelenkaWed, 11 Feb 2015 11:56:34 +0000
                            • Jakub ZelenkaSun, 15 Feb 2015 20:18:16 +0000
                              • Anatol BelskiTue, 17 Feb 2015 16:53:28 +0000
                                • Anatol BelskiSun, 22 Feb 2015 18:09:50 +0000
                                  • Jakub ZelenkaSun, 22 Feb 2015 22:05:45 +0000
  • Jan EhrhardtMon, 09 Feb 2015 07:48:53 +0000Re: new json, push generated file?
    • Pierre JoyeMon, 09 Feb 2015 07:55:58 +0000Re: Re: new json, push generated file?
  • Nikita PopovMon, 09 Feb 2015 19:22:56 +0000
    • Jakub ZelenkaMon, 09 Feb 2015 20:12:26 +0000