1--TEST-- 2Bug #73793 (WDDX uses wrong decimal separator) 3--SKIPIF-- 4<?php 5if (!extension_loaded('wddx')) print 'skip wddx extension not available'; 6if (setlocale(LC_NUMERIC, ['de_DE', 'de_DE.UTF-8', 'de-DE']) === false) { 7 print 'skip German locale not available'; 8} 9?> 10--FILE-- 11<?php 12setlocale(LC_NUMERIC , ['de_DE', 'de_DE.UTF-8', 'de-DE']); 13var_dump(wddx_serialize_value(['foo' => 5.1])); 14?> 15===DONE=== 16--EXPECT-- 17string(120) "<wddxPacket version='1.0'><header/><data><struct><var name='foo'><number>5.1</number></var></struct></data></wddxPacket>" 18===DONE=== 19