add alias for redis_host (used in smile_redis_session_store)

docker_dev_start.py

@@ -484,6 +484,16 @@
                 'options',
                 'db_password',
             )
+        # doing this avoid having to change the value of redis_host
+        # used by smile_redis_session_store
+        redis_host = (
+             cp_local.has_section('options') and
+             cp_local.has_option('options', 'redis_host') and
+             cp_local.get('options', 'redis_host')) or None
+        if redis_host:
+            print('add redis host')
+            options.append('--add-host')
+            options.append('{}:{}'.format(redis_host, local_ip))
     # default values if nothing else
     if not user:
         user = 'odoo'